Iowa Type Theory Commute

Introduction to Formalizing Programming Languages Theory

12 min • 25 november 2024

In this episode, I begin discussing the question and history of formalizing results in Programming Languages Theory using interactive theorem provers like Rocq (formerly Coq) and Agda.

Senaste avsnitt

Podcastbild

00:00 -00:00
00:00 -00:00