Iowa Type Theory Commute

Latest Episodes:

The Lean Prover Feb 27, 2022

Show notes

In this episode, I talk about what I have learned so far about the Lean prover, especially from an excellent (if somewhat advanced) Master's thesis, "The Type Theory of Lean" by Marco Garneiro.

More on Isabelle, and the Complexity of ITPs Feb 16, 2022

Show notes

I talk about my attempts to use Isabelle as a newbie, and reflect a little on the complexity of both Isabelle and Coq.

Isabelle/HOL Jan 27, 2022

Show notes

The Isabelle theorem prover supports different logics, but its most developed seems to be Higher-Order Logic (HOL). In this episode, I talk about the logic and approach of Isabelle/HOL, as far as I have understood them.

More on Agda Jan 12, 2022

Show notes

I talk a bit more about the Agda proof assistant.

A look at Agda Jan 09, 2022

Show notes

In this episode I talk a bit about the Agda proof assistant.

More reflections on Coq Dec 31, 2021

Show notes

I talk about a couple good resources for learning Coq, the problem of too many ways to do things in type theory, and issues trying to explain and document a very complex language.

The Coq Proof Assistant Dec 28, 2021

Show notes

I discuss Coq, a widely used proof assistant based on a constructive type theory. One episode definitely cannot do justice to the complexity of a tool like this -- but I take a first try at covering its features at a high level.

Introduction to Interactive Theorem Provers Dec 16, 2021

Show notes

This is the start of Chapter 15, about interactive theorem provers (ITPs). In this episode, I talk about the difference between fully automatic and interactive provers, and my plan to discuss and compare several different ITPs, in future episodes of this chapter.

The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0 Dec 10, 2021

Show notes

In this episode, I outline the argument for why the proof-theoretic ordinal (in the sense of Rathjen, as presented last episode) is epsilon-0. My explanation has something of a hole, in explaining how one would go about deriving induction for ordinals strictly less than epsilon-0 in Peano Arithmetic. To help paper over this hole a little, I discuss a really nice recent exposition of encoding ordinals in Agda.

The proof-theoretic ordinal of a logical theory Nov 20, 2021

Show notes

Ordinal analysis seeks to determine the strength of a logical theory by assigning an ordinal to it. Which one? In this episode I describe a definition of the proof-theoretic ordinal of a logical theory from a paper by proof theorist Michael Rathjen. It is basically a measure of how strong an induction principle is derivable in the theory. (The first parts of the paper are pretty accessible, but the rest gets hard, at least for me.)

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