Podcasts by Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Further podcasts by Aaron Stump
Podcast on the topic Technologie
All episodes
Identity Inclusion in Relational Type Theory from 2021-01-31T22:10:42.023393
Where relational semantics for parametric polymorphism often includes a lemma called Identity Extension (discussed in Episode 10, on the paper "Types, Abstraction, and Parametric Polymorphism"), Re...
ListenOn the paper "The Girard-Reynolds Isomorphism" by Philip Wadler from 2021-01-31T22:10:42.023393
I give a brief glimpse at Phil Wadler's important paper "The Girard-Reynolds Isomorphism", which is quite relevant for Relational Type Theory as it shows that relational semantics for the usual typ...
ListenEquivalence of inductive and parametric naturals in RelTT from 2021-01-31T22:10:42.023393
I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent. This is similar to proofs one can find in a paper of Ph...
ListenExamples in Relational Type Theory from 2021-01-31T22:10:42.023393
I discuss how to define internalized relational typings, implicit products, and two forms of natural number types, in RelTT.
ListenThe Semantics of Relational Types from 2021-01-31T22:10:42.023393
In this episode, I discuss the semantics of the proposed six type constructors of RelTT.
ListenThe Types of Relational Type Theory from 2021-01-31T22:10:42.023393
This episode continues the introduction of RelTT by presenting the types of the language. Because the system is based on binary relational semantics, we can include binary relational operators lik...
ListenIntroducing Relational Type Theory from 2021-01-31T22:10:42.023393
This episode begins Chapter 11 of the podcast, on Relational Type Theory. This is a new approach to type theory that I am developing. The idea is to design a type system based on the binary relat...
ListenOn the paper "Types, Abstraction, and Parametric Polymorphism" from 2021-01-31T22:10:42.023393
In this episode I discuss one of the greatest papers in the history of Programming Language's research, namely "Types, Abstraction, and Parametric Polymorphism" by the great John C. Reynolds. I su...
ListenParametric models and representation independence from 2021-01-31T22:10:42.023393
Today I discuss the construction of relational models of typed lambda calculus (say, System F), that support the idea of representation independence. This is a feature of a type theory where diffe...
ListenExplaining my encoding of a HOAS datatype, part 2 from 2021-01-31T22:10:42.023393
I continue discussing the approach to HOAS from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page.
ListenExplaining my encoding of a HOAS datatype, part 1 from 2021-01-31T22:10:42.023393
I start explaining an idea from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page. The goal is to encode a datatype (including its c...
ListenTerm models for higher-order signatures from 2021-01-31T22:10:42.023393
I discuss the problem of term models for higher-order signatures, following a prelude about the Edinburgh Logical Framework (LF) and higher-order datatypes.
ListenLambda applicative structures and interpretations of lambda abstractions from 2021-01-31T22:10:42.023393
Discussion of definitions in "Pre-logical relations" by Honsell and Sannella, particularly the notion of a lambda applicative structure (similar to a definition in John C. Mitchell's book "Foundati...
ListenThe Basic Lemma from 2021-01-31T22:10:42.023393
Also known as the Fundamental Property, this is a theorem stating that for every well-typed term t : T, and every logical relation R between algebraic structures A and B, the meaning of t in A is r...
ListenLogical relations are not closed under composition from 2021-01-31T22:10:42.023393
In this episode, I talk through a small (but intricate) example from a paper titled "Pre-logical relations" by Honsell and Sannella, showing that the set of logical relations is not closed under co...
ListenThe definition of a logical relation from 2021-01-31T22:10:42.023393
Logical relations are the relational generalization of the algebraic concept of a homomorphism -- but they go further in extending the notion of structure-preservation to higher-order structures. ...
ListenIntroduction to Logical Relations from 2021-01-31T22:10:42.023393
Start of Chapter 10, on logical relations and parametricity. Basic idea of logical relation as the relational generalization of the algebraic idea of homomorphism. This is also the start of Seaso...
ListenLamping's abstract algorithm from 2021-01-31T22:10:42.023393
The simplified version of Lamping's algorithm for optimal beta-reduction is discussed. We have duplicators which eat their way through lambda graphs. When copying a lambda abstraction, we send on...
ListenExamples showing non-optimality of Haskell from 2021-01-31T22:10:42.023393
I discuss some examples posted on my blog, QA9, which show that executables produced by ghc (the main implementation of Haskell) can exhibit non-optimal beta-reduction. Thanks to Victor Maia for m...
ListenLambda graphs with duplicators and start of Lamping's abstract algorithm from 2021-01-31T22:10:42.023393
In this episode I talk about how to represent lambda terms as graphs with duplicator nodes for splitting edges corresponding to bound variables. I also start discussing the beginning of Lampings' ...
ListenDuplicating redexes as the central problem of optimal reduction from 2021-01-31T22:10:42.023393
We discussed last time how with a graph-sharing implementation of untyped lambda calculus, it can happen that you are forced to break sharing and copy a lambda abstraction. We discuss in this epis...
ListenIntroduction to optimal beta reduction from 2021-01-31T22:10:42.023393
Some background on optimal beta reduction: Levy, Lamping. The main problem to overcome is duplicating a lambda abstraction that is used in two different places in your term. The solution is to tr...
ListenLexicographic termination from 2021-01-31T22:10:42.023393
Many termination checkers support lexicographic (structural) recursion. The lexicographic combination of orderings on sets A and B is an ordering on A x B where a pair decreases if the A component...
ListenMendler-style iteration from 2021-01-31T22:10:42.023393
Another type-based approach to termination-checking for recursive functions over inductive datatypes is to use so-called Mendler-style iteration. On this approach, we write recursive functions by ...
ListenWell-founded recursion from 2021-01-31T22:10:42.023393
Well-founded recursion is a technique to turn recursion which decreases along a well-founded ordering into a structural recursion.
ListenCompositional termination checking with sized types from 2021-01-31T22:10:42.023393
Discussion of a compositional method of termination checking using so-called sized types. Datatypes are indexed by sizes, and recursive calls can only be made on data of strictly smaller size than...
ListenNoncompositionality of syntactic structural-recursion checks from 2021-01-31T22:10:42.023393
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 m...
ListenStructural termination from 2021-01-31T22:10:42.023393
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...
ListenProving Confluence for Untyped Lambda Calculus II from 2021-01-31T22:10:42.023393
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!
ListenProving Confluence for Untyped Lambda Calculus I from 2021-01-31T22:10:42.023393
Start of discussion on how to prove confluence for untyped lambda calculus. Also some discussion about the research community interested in confluence.
ListenConfluence, and its use for conversion checking from 2021-01-31T22:10:42.023393
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 ...
ListenNormalization and logical consistency from 2021-01-31T22:10:42.023393
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...
ListenNormalization in type theory: where it is needed, and where not from 2021-01-31T22:10:42.023393
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. Tra...
ListenIntroduction to normalization from 2021-01-31T22:10:42.023393
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 ...
ListenProving type safety; upcoming metatheoretic properties from 2021-01-31T22:10:42.023393
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 ...
ListenThe progress property and the problem of axioms in type theory from 2021-01-31T22:10:42.023393
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...
ListenIntroduction to type safety from 2021-01-31T22:10:42.023393
Type safety is a basic property of both statically typed programming languages and type theories. It has traditionally (past few decades) been decomposed into type preservation and progress. Type...
ListenIntroduction to metatheory from 2021-01-31T22:10:42.023393
Metatheory is concerned with proving properties about theories, in this case type theories or programming languages.
ListenDefinition of the Mendler encoding from 2021-01-31T22:10:42.023393
We consider using Mendler's technique of abstracting out problematic types with new type variables, and how this can yield a lambda encoding where the programmer is in charge of when to make recurs...
ListenThe Mendler encoding and the problem of explicit recursion from 2021-01-31T22:10:42.023393
The Church encoding allows definition of certain recursive functions, but all the recursive calls are implicit. The encoding simply presents you with the results of recursion for all immediate sub...
ListenThe Scott encoding from 2021-01-31T22:10:42.023393
In this episode we briefly review the Church and Parigot encodings (discussed previously in Chapter 6 of this podcast) and then consider the Scott encoding, where combining functions receive only t...
ListenMore on the Parigot encoding from 2021-01-31T22:10:42.023393
The Parigot encoding has exponential-size normal forms: but don't panic! With a decent graph-sharing implementation of lambda calculus, they take linear space in memory.
ListenIntroduction to the Parigot encoding from 2021-01-31T22:10:42.023393
The Parigot encoding solves the Church encoding's problem of inefficient predecessor. It can be typed using positive-recursive types, which preserve normalization of the type theory.
ListenChurch-encoding natural numbers from 2021-01-31T22:10:42.023393
What is fold-right for a natural number? How do we define addition with this? The problem of inefficient predecessor.
ListenChurch encoding of lists from 2021-01-31T22:10:42.023393
We consider fold-right for lists, and its static type. The Church encoding for lists makes them into their own fold-right functions
ListenChurch encoding of the booleans from 2021-01-31T22:10:42.023393
The Church encoding represents data as their own fold-right functions. For booleans, this means they become their own if-then-else expressions. We consider the polymorphic type for these, which i...
ListenIntroduction to Church encoding from 2021-01-31T22:10:42.023393
The Church encoding represents data as their own fold-right functions
ListenFunctional encodings turning the world inside out from 2021-01-31T22:10:42.023393
Functional encodings take programming language features like pattern-matching and recursion and move them from outside of data to inside of data.
ListenMore benefits of lambda encodings from 2021-01-31T22:10:42.023393
The idea that without lambda encodings, the current state of the art forces you to commit to a class of datatypes in the design of your type theory.
ListenIntroduction to lambda encodings from 2021-01-31T22:10:42.023393
A lambda encoding is some way of representing data as functions (lambda abstractions). Some motivations for this for computer-checked proofs and type theory.
ListenIntersection types using Curry-style typing from 2021-01-31T22:10:42.023393
With Curry-style typing, we may define intersection types to internalize the idea that a term has two types
ListenCurry-style versus Church-style, and the nature of type annotations from 2021-01-31T22:10:42.023393
Considering erased versus non-erased type annotations
ListenMore on Computation First, and Basic Idea of Realizability from 2021-01-31T22:10:42.023393
A basic example of realizability, to show how types are defined in terms of computation
ListenTypes should be erased for executing and reasoning about programs from 2021-01-31T22:10:42.023393
Computation comes first, types come second
ListenWhy go beyond GADTs? from 2021-01-31T22:10:42.023393
What are some reasons for true dependent types instead of GADTs? What are some language-design choices for going beyond GADTs?
ListenGADTs for programming with representations of types from 2021-01-31T22:10:42.023393
Review of previous GADT examples we discussed, and a new one on runtime type representations
ListenUsing GADTs for typed subsetting of your language from 2021-01-31T22:10:42.023393
GADTs allow datatypes for the typed syntax trees of subsets of your language
ListenExample of programming with indexed types: binary search trees from 2021-01-31T22:10:42.023393
The example of binary search trees where we use indices to enforce the bst property statically
ListenProgramming with indexed types using singletons from 2021-01-31T22:10:42.023393
Singleton types connect program expressions with value in the index domain
ListenLimitations of indexed types that are not truly dependent from 2021-01-31T22:10:42.023393
Limitations of programming with indexed types
ListenProgramming with Indexed Types from 2021-01-31T22:10:42.023393
Programming with indexed types like vectors
ListenProgram Termination and the Curry-Howard Isomorphism from 2021-01-31T22:10:42.023393
Why termination is needed for Curry-Howard, and how it is usually enforced
ListenWhy Curry-Howard for classical proofs is a bad idea for programming from 2021-01-31T22:10:42.023393
Why it is not a good idea to use computational classical type theory for programming
ListenCurry-Howard for classical logic from 2021-01-31T22:10:42.023393
Amazingly, nonconstructive proofs can also be given a computational interpretation, using control operators
ListenDependent types and design by contract from 2021-01-31T22:10:42.023393
Dependent types allow you to express contracts of functions in their types
ListenIndexed types and Curry-Howard for first-order quantifiers from 2021-01-31T22:10:42.023393
First-order quantifiers under CH are for types indexed by expressions from a different syntactic category than programs
ListenThe Curry-Howard Isomorphism for Propositional Logic from 2021-01-31T22:10:42.023393
The Curry-Howard isomorphism for propositional connectives like conjunction and implication
ListenThe Curry-Howard Isomorphism for Induction from 2021-01-31T22:10:42.023393
Under the Curry-Howard isomorphism, mathematical induction is identified with terminating recursion
ListenConstructive proofs as programs from 2021-01-31T22:10:42.023393
Constructive proofs are essentially programs; several simple examples
ListenIntroduction to the Curry-Howard Isomorphism from 2021-01-31T22:10:42.023393
Beginning discussion of the Curry-Howard isomorphism, also constructive versus nonconstructive proofs
ListenFunctors and catamorphisms from 2021-01-31T22:10:42.023393
More about the structured recursion scheme known as catamorphism, and functor basics
ListenStructured Recursion Schemes for Point-Free Recursion from 2021-01-31T22:10:42.023393
Category theory and point-free programming using structured recursion schemes
ListenMore on point-free programming and category theory from 2021-01-31T22:10:42.023393
A few basic ideas from category theory, and the problem of understanding very concise code
ListenPoint-free programming and category theory from 2021-01-31T22:10:42.023393
Relation of point-free functional programming to category theory.
ListenConcise code through point-free programming from 2021-01-31T22:10:42.023393
Basic idea of point-free functional programming
ListenMore on FP and concise code from 2021-01-31T22:10:42.023393
Datatype support in functional languages is very useful for concise language-processing programs
ListenFunctional Programming and Concise Code: Type Inference from 2021-01-31T22:10:42.023393
Start of discussion on how functional programming leads to more concise code; type inference
ListenIntroduction to Functional Programming from 2021-01-31T22:10:42.023393
Basic idea of functional programming, including three different kinds: with mutable state, without, and strong
ListenSoftware Engineering Considerations for Formal Methods from 2021-01-31T22:10:42.023393
Different kinds of software merit different levels of effort for verification
ListenPower of Computer-Checked Proofs for Software from 2021-01-31T22:10:42.023393
Rationale for formal methods for software
ListenTechnical reasons for lack of adoption of computer-checked proofs from 2021-01-31T22:10:42.023393
More discussion of reasons for lack of adoption of computer-checked proofs
ListenWhy Computer-Checked Proofs are Not Used More in Mathematics from 2021-01-31T22:10:42.023393
Discussion of reasons more mathematicians have not adopted computer-checked proofs
ListenComputer-Checked Proofs in American Research from 2021-01-31T22:10:42.023393
Recent history of computer-checked proofs in American Computer Science research
ListenComputer-checked proofs about software from 2021-01-31T22:10:42.023393
Discussion of the idea that computer-checked proofs can ensure properties of software
ListenMore on Computer-Checked Proofs from 2021-01-31T22:10:42.023393
Examples of computer-checked proofs in Math and Computer Science
ListenComputer-checked proofs from 2019-11-21T14:00
First episode of the Iowa Type Theory Commute. The basic idea of computer-checked proofs. The example of the original proof of the Four Color Theorem.
ListenComputer-checked proofs from 2019-11-21T14:00
First episode of the Iowa Type Theory Commute. The basic idea of computer-checked proofs. The example of the original proof of the Four Color Theorem.
Listen