Iowa Type Theory Commute
Episodes
On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler
18 Jan 2021
Contributed by Lukas
I give a brief glimpse at Phil Wadler's important paper "The Girard-Reynolds Isomorphism", which is quite relevant for Relational Type ...
Equivalence of inductive and parametric naturals in RelTT
28 Dec 2020
Contributed by Lukas
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...
Examples in Relational Type Theory
23 Dec 2020
Contributed by Lukas
I discuss how to define internalized relational typings, implicit products, and two forms of natural number types, in RelTT.
The Semantics of Relational Types
23 Dec 2020
Contributed by Lukas
In this episode, I discuss the semantics of the proposed six type constructors of RelTT.
Introducing Relational Type Theory
15 Dec 2020
Contributed by Lukas
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 ...
The Types of Relational Type Theory
15 Dec 2020
Contributed by Lukas
This episode continues the introduction of RelTT by presenting the types of the language. Because the system is based on binary relational semantics...
On the paper "Types, Abstraction, and Parametric Polymorphism"
26 Nov 2020
Contributed by Lukas
In this episode I discuss one of the greatest papers in the history of Programming Language's research, namely "Types, Abstraction, and Para...
Parametric models and representation independence
09 Nov 2020
Contributed by Lukas
Today I discuss the construction of relational models of typed lambda calculus (say, System F), that support the idea of representation independence. ...
Explaining my encoding of a HOAS datatype, part 2
09 Nov 2020
Contributed by Lukas
I continue discussing the approach to HOAS from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, avail...
Explaining my encoding of a HOAS datatype, part 1
19 Oct 2020
Contributed by Lukas
I start explaining an idea from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web...
Term models for higher-order signatures
19 Oct 2020
Contributed by Lukas
I discuss the problem of term models for higher-order signatures, following a prelude about the Edinburgh Logical Framework (LF) and higher-order data...
Lambda applicative structures and interpretations of lambda abstractions
08 Oct 2020
Contributed by Lukas
Discussion of definitions in "Pre-logical relations" by Honsell and Sannella, particularly the notion of a lambda applicative structure (sim...
The Basic Lemma
30 Sep 2020
Contributed by Lukas
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...
Logical relations are not closed under composition
31 Aug 2020
Contributed by Lukas
In this episode, I talk through a small (but intricate) example from a paper titled "Pre-logical relations" by Honsell and Sannella, showing...
The definition of a logical relation
19 Aug 2020
Contributed by Lukas
Logical relations are the relational generalization of the algebraic concept of a homomorphism -- but they go further in extending the notion of struc...
Introduction to Logical Relations
17 Aug 2020
Contributed by Lukas
Start of Chapter 10, on logical relations and parametricity. Basic idea of logical relation as the relational generalization of the algebraic idea o...
Lamping's abstract algorithm
25 Jul 2020
Contributed by Lukas
The simplified version of Lamping's algorithm for optimal beta-reduction is discussed. We have duplicators which eat their way through lambda g...
Examples showing non-optimality of Haskell
15 Jul 2020
Contributed by Lukas
I discuss some examples posted on my blog, QA9, which show that executables produced by ghc (the main implementation of Haskell) can exhibit non-optim...
Lambda graphs with duplicators and start of Lamping's abstract algorithm
03 Jul 2020
Contributed by Lukas
In this episode I talk about how to represent lambda terms as graphs with duplicator nodes for splitting edges corresponding to bound variables. I a...
Duplicating redexes as the central problem of optimal reduction
21 Jun 2020
Contributed by Lukas
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...
Introduction to optimal beta reduction
16 Jun 2020
Contributed by Lukas
Some background on optimal beta reduction: Levy, Lamping. The main problem to overcome is duplicating a lambda abstraction that is used in two diffe...
Lexicographic termination
03 Jun 2020
Contributed by Lukas
Many termination checkers support lexicographic (structural) recursion. The lexicographic combination of orderings on sets A and B is an ordering on...
Well-founded recursion
19 May 2020
Contributed by Lukas
Well-founded recursion is a technique to turn recursion which decreases along a well-founded ordering into a structural recursion.
Mendler-style iteration
19 May 2020
Contributed by Lukas
Another type-based approach to termination-checking for recursive functions over inductive datatypes is to use so-called Mendler-style iteration. On...
Compositional termination checking with sized types
30 Mar 2020
Contributed by Lukas
Discussion of a compositional method of termination checking using so-called sized types. Datatypes are indexed by sizes, and recursive calls can on...
Noncompositionality of syntactic structural-recursion checks
20 Mar 2020
Contributed by Lukas
Review of need for termination analysis for recursive functions on inductive datatypes. Discussion of a serious problem with syntactic termination c...
Structural termination
17 Mar 2020
Contributed by Lukas
Start of Chapter 8 of the podcast, on termination checking in type theory, and strong functional programming. Discussion of a little history of addi...
Proving Confluence for Untyped Lambda Calculus II
13 Mar 2020
Contributed by Lukas
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 ...
Proving Confluence for Untyped Lambda Calculus I
13 Mar 2020
Contributed by Lukas
Start of discussion on how to prove confluence for untyped lambda calculus. Also some discussion about the research community interested in confluen...
Confluence, and its use for conversion checking
11 Mar 2020
Contributed by Lukas
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 reduct...
Normalization and logical consistency
09 Mar 2020
Contributed by Lukas
Discussion of the connection between normalization and logical consistency. One approach is to prove normalization and type preservation, to show (i...
Normalization in type theory: where it is needed, and where not
06 Mar 2020
Contributed by Lukas
Normalization (every term reaches a normal form via some reduction sequence) is needed essentially in type theory due to the Curry-Howard isomorphism:...
Introduction to normalization
06 Mar 2020
Contributed by Lukas
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)...
Proving type safety; upcoming metatheoretic properties
04 Mar 2020
Contributed by Lukas
Type safety proofs are big confirmations requiring consideration of all your operational and typing rules. So they rarely contain much deep insight,...
The progress property and the problem of axioms in type theory
04 Mar 2020
Contributed by Lukas
We review the metatheoretic property of type safety, decomposed into two properties called type preservation and progress. Discussion of progress in...
Introduction to type safety
02 Mar 2020
Contributed by Lukas
Type safety is a basic property of both statically typed programming languages and type theories. It has traditionally (past few decades) been decom...
Introduction to metatheory
28 Feb 2020
Contributed by Lukas
Metatheory is concerned with proving properties about theories, in this case type theories or programming languages.
Definition of the Mendler encoding
26 Feb 2020
Contributed by Lukas
We consider using Mendler's technique of abstracting out problematic types with new type variables, and how this can yield a lambda encoding wher...
The Mendler encoding and the problem of explicit recursion
25 Feb 2020
Contributed by Lukas
The Church encoding allows definition of certain recursive functions, but all the recursive calls are implicit. The encoding simply presents you wit...
The Scott encoding
24 Feb 2020
Contributed by Lukas
In this episode we briefly review the Church and Parigot encodings (discussed previously in Chapter 6 of this podcast) and then consider the Scott enc...
More on the Parigot encoding
22 Feb 2020
Contributed by Lukas
The Parigot encoding has exponential-size normal forms: but don't panic! With a decent graph-sharing implementation of lambda calculus, they ta...
Introduction to the Parigot encoding
18 Feb 2020
Contributed by Lukas
The Parigot encoding solves the Church encoding's problem of inefficient predecessor. It can be typed using positive-recursive types, which pre...
Church-encoding natural numbers
17 Feb 2020
Contributed by Lukas
What is fold-right for a natural number? How do we define addition with this? The problem of inefficient predecessor.
Church encoding of lists
15 Feb 2020
Contributed by Lukas
We consider fold-right for lists, and its static type. The Church encoding for lists makes them into their own fold-right functions
Church encoding of the booleans
15 Feb 2020
Contributed by Lukas
The Church encoding represents data as their own fold-right functions. For booleans, this means they become their own if-then-else expressions. We...
Introduction to Church encoding
12 Feb 2020
Contributed by Lukas
The Church encoding represents data as their own fold-right functions
Functional encodings turning the world inside out
11 Feb 2020
Contributed by Lukas
Functional encodings take programming language features like pattern-matching and recursion and move them from outside of data to inside of data.
More benefits of lambda encodings
07 Feb 2020
Contributed by Lukas
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.
Introduction to lambda encodings
07 Feb 2020
Contributed by Lukas
A lambda encoding is some way of representing data as functions (lambda abstractions). Some motivations for this for computer-checked proofs and typ...
Adding a top type and allowing non-normalizing terms
05 Feb 2020
Contributed by Lukas
Curry-style typing and realizability make it sensible to allow a top type to type every term, even non-normalizing ones.
Intersection types using Curry-style typing
04 Feb 2020
Contributed by Lukas
Intersection types internalize the idea that a term has two types. Curry-style typing is generally needed for this to be nontrivial.
Curry-style versus Church-style, and the nature of type annotations
30 Jan 2020
Contributed by Lukas
In Curry-style typing annotations -- for example, the types of bound variables -- are erased, and not truly (semantically) part of the term. In Chur...
More on Computation First, and Basic Idea of Realizability
29 Jan 2020
Contributed by Lukas
Types are specifications whose semantics is explained in terms of computation, which is thus conceptually prior. Realizability is a way of explainin...
Types should be erased for executing and reasoning about programs
29 Jan 2020
Contributed by Lukas
In which I argue that type information should be erased from programs by the compiler both for final execution and also for reasoning (in a language w...
Why go beyond GADTs?
24 Jan 2020
Contributed by Lukas
GADTs are quite powerful. Why go all the way to true dependent types? And should you use the Curry-Howard isomorphism (see Chapter 3 of the podcas...
GADTs for programming with representations of types
22 Jan 2020
Contributed by Lukas
This episode reviews some of the applications of GADTs we have discussed so far, and discusses an example where we want to write a function that consu...
Using GADTs for typed subsetting of your language
20 Jan 2020
Contributed by Lukas
One use case for GADTs (as a special case of dependent types) is to form a typed subset of your host language. One creates an EDSL called Expr a, wh...
Example of programming with indexed types: binary search trees
16 Jan 2020
Contributed by Lukas
Using indexed types, we can restrict the form of legal values in some datatype. A nice example is binary search trees, where we can statically enfor...
Programming with indexed types using singletons
16 Jan 2020
Contributed by Lukas
Basic idea of using singleton types like Nat n where n is a value from the index domain, to connect program expressions and index expressions. The d...
Limitations of indexed types that are not truly dependent
14 Jan 2020
Contributed by Lukas
If indices to types come from a different syntactic category than programs, there are a few things you cannot do. Some initial thoughts on how to wo...
Programming with Indexed Types
13 Jan 2020
Contributed by Lukas
Indexed datatypes like vectors, where the indices come from a different syntactic category than program expressions.
Program Termination and the Curry-Howard Isomorphism
10 Jan 2020
Contributed by Lukas
For programs to make sense as proofs, they need to be terminating (cannot run forever), since otherwise you can write infinite loops that have any typ...
Why Curry-Howard for classical proofs is a bad idea for programming
07 Jan 2020
Contributed by Lukas
If you have dependent types, classical reasoning, and the Curry-Howard isomorphism, you can write programs that look like they are invoking oracles fo...
Curry-Howard for classical logic
06 Jan 2020
Contributed by Lukas
CH can be applied to classical logic, too. The seminal paper is <a href="https://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf">A ...
Dependent types and design by contract
04 Jan 2020
Contributed by Lukas
Dependent types are discussed, particularly as used for expressing pre- and post-conditions of functions.
Indexed types and Curry-Howard for first-order quantifiers
03 Jan 2020
Contributed by Lukas
I follow up on some comments I made about Curry-Howard for first-order quantifiers in the previous episode. Sheard's Omega language also mentio...
The Curry-Howard Isomorphism for Propositional Logic
02 Jan 2020
Contributed by Lukas
Discussion of the Curry-Howard isomorphism for the connectives of propositional logic (AND, OR, NOT, FALSE, IMPLIES). Initial consideration of Curry...
The Curry-Howard Isomorphism for Induction
31 Dec 2019
Contributed by Lukas
In which I discover why the domino analogy for explaining induction always bothered me!
Constructive proofs as programs
22 Dec 2019
Contributed by Lukas
We consider the basic idea of the Curry-Howard isomorphism, that constructive proofs are essentially programs, and vice versa. Several simple exampl...
Functors and catamorphisms
20 Dec 2019
Contributed by Lukas
More about the structured recusion scheme known as the catamorphism. Basic idea of functors.
Introduction to the Curry-Howard Isomorphism
20 Dec 2019
Contributed by Lukas
The basic idea of the Curry-Howard isomorphism, and its connection to the contents of Chapters 1 and 2. Constructive proof. A famous nonconstructi...
Structured Recursion Schemes for Point-Free Recursion
19 Dec 2019
Contributed by Lukas
Review of basic application of category theory for functional programming. Recursion schemes are combinators that let you write point-free recursion...
More on point-free programming and category theory
17 Dec 2019
Contributed by Lukas
A few very basic ideas of categories and combinators. Also, the problem of understanding very concise code.
Point-free programming and category theory
17 Dec 2019
Contributed by Lukas
Relation of point-free functional programming to category theory.
Concise code through point-free programming
13 Dec 2019
Contributed by Lukas
Higher-order functions help make it possible to program in a point-free style, where we use combinators to connect functions, rather than calling the ...
More on FP and concise code
12 Dec 2019
Contributed by Lukas
Discussion of datatypes for tree-like data structures in functional languages. Usefulness of these for processing structured linguistic artifacts, w...
Functional Programming and Concise Code: Type Inference
12 Dec 2019
Contributed by Lukas
Start of discussion of some of technology and culture that lead to more concise code in functional programming languages. Type inference to avoid wr...
Introduction to Functional Programming
11 Dec 2019
Contributed by Lukas
Introduction to the basic idea of functional programming. Three kinds are discussed: functional programming with mutable state, pure functional prog...
Software Engineering Considerations for Formal Methods
02 Dec 2019
Contributed by Lukas
Discussion of some practicalities of applying formal methods to software. Ideally we are seeking techniques that can be applied with increasing effo...
Power of Computer-Checked Proofs for Software
01 Dec 2019
Contributed by Lukas
Continuing pessimistic discussion about the purpose of formal methods for Computer Science. But then counter arguments about the value of absolutely...
Technical reasons for lack of adoption of computer-checked proofs
28 Nov 2019
Contributed by Lukas
Discussion of a technical reason for lack of adoption of computer-checked proofs for mathematics, namely the level of detail in the proof. Proof ass...
Why Computer-Checked Proofs are Not Used More in Mathematics
27 Nov 2019
Contributed by Lukas
Some discussion of why computer-checked proofs have not been adopted more in mathematics. The psychology of telling mathematicians their time-honore...
Computer-Checked Proofs in American Research
26 Nov 2019
Contributed by Lukas
Some pockets of interest in computer-checked proofs in the US in the 1980s and 1990s. Several important research projects and initiatives in the US ...
Computer-checked proofs about software
24 Nov 2019
Contributed by Lukas
Computer-checked proofs can ensure properties of software. Discussion of several aspects of this idea.
More on Computer-Checked Proofs
22 Nov 2019
Contributed by Lukas
Further discussion of computer-checked proofs, including the example of the proof by Hales and his collaborators of the Kepler Conjecture. Automath ...
Computer-checked proofs
21 Nov 2019
Contributed by Lukas
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 Theo...