Iowa Type Theory Commute

Latest Episodes:

Introducing Relational Type Theory Dec 14, 2020

Show notes

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 relational semantics for types, which we considered in Chapter 10. This episode recalls some of that semantics.

On the paper "Types, Abstraction, and Parametric Polymorphism" Nov 25, 2020

Show notes

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 summarize the two interconnected semantics for polymorphic types proposed by Reynolds: one which interprets types as sets and programs as members of those sets, and another which interprets types as relations on the sets from the first interpretation. Listen and you will get to hear my aha moment as I understand live on air what the Identity Extension Lemma really means. See also this blog post on the same topic.

Parametric models and representation independence Nov 09, 2020

Show notes

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 different implementations of the same interface can be proved equivalent, and used interchangeably in the theory. Only in the past couple years have researchers proposed theories like this, but the semantic ideas underlying such theories have been around since Reynolds's seminal paper "Types, Abstraction, and Parametric Polymorphism".

Explaining my encoding of a HOAS datatype, part 2 Nov 09, 2020

Show notes

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.

Explaining my encoding of a HOAS datatype, part 1 Oct 19, 2020

Show notes

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 constructors, which we saw were troublesome for higher-order signatures generally in the previous episode) for application-free lambda terms, which I submit is the simplest higher-order datatype possible. I just explain some of the setup, and will attempt wading through the details next time.

Term models for higher-order signatures Oct 19, 2020

Show notes

I discuss the problem of term models for higher-order signatures, following a prelude about the Edinburgh Logical Framework (LF) and higher-order datatypes.

Lambda applicative structures and interpretations of lambda abstractions Oct 07, 2020

Show notes

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 "Foundations for Programming Languages'). In short, lambda abstractions get interpreted in combinatory algebras by compiling away the lambda abstractions in favor of S and K combinators, which are then interpreted by the combinatory algebra. I complain about the fact that the definition of a lambda applicative structure is required to come with an interpretation function for terms (hence tying the semantics to the syntax).

The Basic Lemma Sep 30, 2020

Show notes

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 related by R to the meaning of t in B. I view it as a straightforward semantic soundness property, but where the semantics of types is this somewhat interesting one that interprets types as binary relations on structures A and B. I muse on these matters a bit in the episode.

Logical relations are not closed under composition Aug 31, 2020

Show notes

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 composition. That is, you can have a logical relation between structure A and structure B, and one between B and C, but the composition (while a relation) is not a logical relation between A and C. This took me three takes to get to where I wasn't tripping over my tongue, so enjoy.

The definition of a logical relation Aug 18, 2020

Show notes

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. We discuss the basic definition in this episode.

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected

Our TOPPODCAST Picks

Follow Us

Stay Connected

Iowa Type Theory Commute

Related Podcasts

1

2

3

4

5

6