EPISODE · Dec 29, 2021 · 15 MIN
The Coq Proof Assistant
from Iowa Type Theory Commute · host Aaron Stump
I discuss Coq, a widely used proof assistant based on a constructive type theory. One episode definitely cannot do justice to the complexity of a tool like this -- but I take a first try at covering its features at a high level.
What this episode covers
I discuss Coq, a widely used proof assistant based on a constructive type theory. One episode definitely cannot do justice to the complexity of a tool like this -- but I take a first try at covering its features at a high level.
NOW PLAYING
The Coq Proof Assistant
No transcript for this episode yet
Similar Episodes
Mar 4, 2026 ·7m
Feb 22, 2026 ·9m
Feb 8, 2026 ·11m
Feb 2, 2026 ·12m
Jan 30, 2026 ·31m
Jan 29, 2026 ·39m