Start / Iowa Type Theory Commute / The progress property and the problem of axioms in type theory

Iowa Type Theory Commute

The progress property and the problem of axioms in type theory

10 min • 4 mars 2020

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.

Senaste avsnitt

Correction: the Correct Author of the Proof from Last Episode, and an AI flop

12 maj | 7 min

Krivine's Proof of FD, Using Intersection Types

5 maj | 22 min

A Measure-Based Proof of Finite Developments

16 april | 23 min

Introduction to the Finite Developments Theorem

27 mars | 16 min

Nominal Isabelle/HOL

31 januari | 16 min
Vad är en podd?

En liten tjänst av I'm With Friends. Finns även på engelska.

Podcastbild

00:00 -00:00
00:00 -00:00