<p>For programs to make sense as proofs, they need to be terminating (cannot run forever), since otherwise you can write infinite loops that have any type.  Under Curry-Howard this means any formula is provable, which is one way to define inconsistency.  (And logics have to be consistent to be useful.)</p>

For programs to make sense as proofs, they need to be terminating (cannot run forever), since otherwise you can write infinite loops that have any type. Under Curry-Howard this means any formula is provable, which is one way to define inconsistency. (And logics have to be consistent to be useful.)

<p>For programs to make sense as proofs, they need to be terminating (cannot run forever), since otherwise you can write infinite loops that have any type.&nbsp; Under Curry-Howard this means any formula is provable, which is one way to define inconsistency.&nbsp; (And logics have to be consistent to be useful.)</p>

Program Termination and the Curry-Howard Isomorphism

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Share Program Termination and the Curry-Howard Isomorphism

Sign up to save your podcasts

Program Termination and the Curry-Howard Isomorphism

Program Termination and the Curry-Howard Isomorphism

More shows like Iowa Type Theory Commute

Dwarkesh Podcast

Type Theory Forall