Podcasts Technology Iowa Type Theory Commute The progress property and the problem of axioms in type theory

The progress property and the problem of axioms in type theory

Published: March 4, 2020, 5 a.m.

b'

We review the metatheoretic property of type safety, decomposed into two properties called type preservation and progress.\\xa0 Discussion of progress in the context of type theory, where adding axioms can lead to a failure of progress.

'