Podcasts Technology Iowa Type Theory Commute Program Termination and the Curry-Howard Isomorphism

Program Termination and the Curry-Howard Isomorphism

Published: Jan. 10, 2020, 8 p.m.

b'

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.\\xa0 Under Curry-Howard this means any formula is provable, which is one way to define inconsistency.\\xa0 (And logics have to be consistent to be useful.)

'