Iowa Type Theory Commute

Latest Episodes:

Noncompositionality of syntactic structural-recursion checks Mar 19, 2020

Show notes

Review of need for termination analysis for recursive functions on inductive datatypes. Discussion of a serious problem with syntactic termination checks, namely noncompositionality. A function may pass the syntactic termination check, but abstracting part of it out into a helper function may result in code which no longer passes the check. So we need a compositional termination check, which will be discussed in subsequent episodes.

Structural termination Mar 17, 2020

Show notes

Start of Chapter 8 of the podcast, on termination checking in type theory, and strong functional programming. Discussion of a little history of adding datatypes to the original pure type theory of Coq (called the Calculus of Constructions). Considering the most basic form of termination checking, which is checking syntactically that recursive calls are only made on subdata of the data input to the recursive function.

Proving Confluence for Untyped Lambda Calculus II Mar 13, 2020

Show notes

Discussion of the basic idea of the Tait--Martin-Loef proof of confluence for untyped lambda calculus. Let me know any requests for what to discuss in Chapter 8!

Proving Confluence for Untyped Lambda Calculus I Mar 13, 2020

Show notes

Start of discussion on how to prove confluence for untyped lambda calculus. Also some discussion about the research community interested in confluence.

Confluence, and its use for conversion checking Mar 11, 2020

Show notes

The basic property of confluence of a nondeterministic reduction semantics: if from starting term t you can reach t1 and also t2 (by two finite reduction sequences), then there is some t3 to which t1 and t2 both reduce in a finite number of steps. The use of confluence for ensuring completeness of the conversion-checking algorithm that tests conversion of t1 and t2 by normalizing both terms and checking for alpha-equivalence (or maybe alpha,eta-equivalence).

Normalization and logical consistency Mar 09, 2020

Show notes

Discussion of the connection between normalization and logical consistency. One approach is to prove normalization and type preservation, to show (in proof-theoretic terms) that all detours can be eliminated from proofs (this is normalization) and that the resulting proof still proves the same theorem (this is type preservation). I mention an alternative I use for Cedille, which is to use a realizability semantics (often used for normalization proofs) directly to prove consistency.

Normalization in type theory: where it is needed, and where not Mar 06, 2020

Show notes

Normalization (every term reaches a normal form via some reduction sequence) is needed essentially in type theory due to the Curry-Howard isomorphism: diverging programs become unsound proofs. Traditionally, type theorists have also desired normalization or even termination (every term reaches a normal form no matter what reduction sequence is explored in a nondeterministic operational semantics) for conversion checking. This is the process of confirming that types are equivalent during type checking, which, due to dependent types, can require checking program equivalence. The latter is usually restricted to just beta-equivalence (where beta-reduction is substitution of argument for input variable when applying a function), because richer notions of program equivalence are usually undecidable. I have a mini-rant in this episode explaining why this usual requirement of normalization for conversion checking is not sensible.
Also I note that you can find the episodes of the podcast organized by chapter on my web page.

Introduction to normalization Mar 05, 2020

Show notes

Discussion of normalization (there is some way to reach a normal form) versus termination (no matter how you execute the term you reach a normal form). A little more discussion of strong FP. For type theory, the need for normalization due to Curry-Howard and due to conversion checking.

Proving type safety; upcoming metatheoretic properties Mar 04, 2020

Show notes

Type safety proofs are big confirmations requiring consideration of all your operational and typing rules. So they rarely contain much deep insight, but are needed to confirm your language's type system is correct. Looking ahead, this episode also talks about the different between normalization and termination when your language is nondeterministic, and the property of confluence.

The progress property and the problem of axioms in type theory Mar 03, 2020

Show notes

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.

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected