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 Philip Wadler's titled "The Girard-Reynolds Isomorphism", which I plan to discuss in the next episode.

I discuss how to define internalized relational typings, implicit products, and two forms of natural number types, in RelTT.

In this episode, I discuss the semantics of the proposed six type constructors of RelTT.

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 like composition and converse as type constructs!  Strange.  The language also promotes terms to relations, by viewing them as functions and then taking their graphs as the relational meaning.

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.

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.

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".

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. 

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.

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