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

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

<p>We review the metatheoretic property of type safety, decomposed into two properties called type preservation and progress.&nbsp; Discussion of progress in the context of type theory, where adding axioms can lead to a failure of progress.</p>

The progress property and the problem of axioms in type theory

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

Share The progress property and the problem of axioms in type theory

Sign up to save your podcasts

The progress property and the problem of axioms in type theory

The progress property and the problem of axioms in type theory