Iowa Type Theory Commute

Turing's proof of normalization for STLC May 20, 2024

In this episode, I describe the first proof of normalization for STLC, written by Alan Turing in the 1940s. See this short note for Turing's original proof and some historical comments.

Introduction to normalization for STLC May 13, 2024

In this episode, after a quick review of the preceding couple, I discuss the property of normalization for STLC, and talk a bit about proof methods. We will look at proofs in more detail in the coming episodes. Feel free to join the Telegram group for the podcast if you want to discuss anything (or just email me at aaron.stump@gmail.com).

The curious case of exponentiation in simply typed lambda calculus May 04, 2024

Like addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC). But surprisingly, the type is non-uniform. If we abbreviate (A -> A) -> A -> A as Nat_A, then exponentiation, which is defined as \ x . \ y . y x, can be assigned type Nat_A -> Nat_(A -> A) -> Nat_A. The second argument needs to have type at strictly higher order than the first argument. This has the fascinating consequence that we cannot define self-exponentiation, \ x . exp x x. That term would reduce to \ x . x x, which is provably not typable in STLC.

Arithmetic operations in simply typed lambda calculus May 04, 2024

It is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STLC). Church-encoded numbers can be given the simple type (A -> A) -> A -> A, for any simple type A. If we abbreviate that type as Nat_A, then addition and multiplication can both be typed in STLC, at type Nat_A -> Nat_A -> Nat_A. Interestingly, things change with exponentiation, which we will consider in the next episode.

More on basics of simple types Apr 29, 2024

I review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.

Begin Chapter on Simple Type Theory Apr 19, 2024

In this episode, after a pretty long hiatus, I start a new chapter on simply typed lambda calculus. I present the typing rules and give some basic examples. Subsequent episodes will discuss various interesting nuances...

Some advanced examples in DCS Sep 24, 2023

This episode presents two somewhat more advanced examples in DCS. They are Harper's continuation-based regular-expression matcher, and Bird's quickmin, which finds the least natural number not in a given list of distinct natural numbers, in linear time. I explain these examples in detail and then discuss how they are implemented in DCS, which ensures that they are terminating on all inputs.

DCS compared to termination checkers for type theories Sep 18, 2023

In this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean. I warmly invite ITTC listeners to experiment with the tool themselves. The repo is here.

Getting started with DCS Sep 09, 2023

In this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute! The repo is here.

Introduction to DCS Sep 03, 2023

DCS is a new functional programming language I am designing and implementing with Stefan Monnier. DCS has a pure, terminating core, around which monads will be layered for possibly diverging, impure computation. In this episode, I talk about this basic design, and its rationale.

Semantics of subtyping Jul 23, 2023

I answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumptive subtyping. The terminology I found in this paper by Zhaohui Luo; see Section 4 of the paper for a comparison of the two kinds of subtyping. With coercive subtyping, we have subtyping axioms "A <: B by c", where c is a function from A to B. The idea is that the compiler should automatically insert calls to c whenever an expression of type A needs to be converted to one of type B. Subsumptive subtyping says that A <: B means that the meaning of A is a subset of the meaning of B. So this kind of subtyping depends on a semantics for types. A simple choice is to interpret a type A as (as least roughly) the set of its inhabitants. So a type like Integer might be interpreted as the set of all integers, etc. Luo argues that subsumptive subtyping does not work for Martin-Loef type theory, where type annotations are inherent parts of terms. For in that situation, A <: B does not imply List A <: List B, because Nil A is an inhabitant of List A but not of List B (which requires instead Nil B).
Join the telegram group here.

More on type inference for simple subtypes Jul 15, 2023

I continue the discussion of Mitchell's paper Type Inference with Simple Subtypes. Coming soon: a discussion of semantics of subtyping.

Subtyping, the golden key Jul 08, 2023

In this episode, I wax rhapsodic for the potential of subtyping to improve the practice of pure functional programming, in particular by allowing functional programmers to drop various irritating function calls that are needed just to make types work out. Examples are lifting functions with monad transformers, or even just the pure/return functions for applicative functors/monads.

Type inference with simple subtypes Jun 29, 2023

In this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell. The paper presents algorithms for computing a type and set of subtype constraints for any term of the pure lambda calculus. I mostly focus here on how subtype constraints allow typing any term (which seems surprising).
You can join the telegram group for discussion related to the podcast.

Basics of subtyping Jun 21, 2023

In this episode, I discuss a few of the basics for what we expect from a subtyping relation on types: reflexivity, transitivity, and the variances for arrow types.

Begin chapter on subtyping Jun 20, 2023

We begin a discussion of subtyping in functional programming. In this episode, I talk about how subtyping is a neglected feature in implemented functional programming languages (for example, not found in Haskell), and how it could be very useful for writing lighter, more elegant code. I also talk about how subtyping could help realize a new vision for practical strong functional programming, where the language has a pure, terminating core language, then a monad for pure but possibly diverging computation, and finally a monad for impurity and divergence.

Last episode discussing Observational Equality Now for Good Apr 13, 2023

In this episode, I conclude my discussion of some (but hardly all!) points from Pujet and Tabareau's POPL 2022 paper, "Observational Equality -- Now for Good!". I talk a bit about the structure of the normalization proof in the paper, which uses induction recursion. See this paper by Peter Dybjer for more about that feature. Also, feel free to join the new Telegram group for the podcast if you want to discuss episodes.

More on observational type theory Mar 23, 2023

I continue discussing the Puject and Tabareau paper, "Observational Equality -- Now for Good", in particular discussing more about how the equality type simplifies based on its index (which is the type of the terms being equated by the equality type), and how proofs of equalities can be used to cast terms from one type to another.
Also, in exciting news, I created a Telegram group that you can join if you want to discuss topics related to the podcast or particularly podcast episodes. I will be monitoring the group. I believe you have to request to join, and then I approve (it might take me until later in the day to do that, just fyi). The invitation link is here.

Introduction to Observational Type Theory Mar 05, 2023

In this episode, I introduce an important paper by Pujet and Tabareau, titled "Observational Equality: Now for Good", that develops earlier work of McBride, Swierstra, and Altenkirch (which I will cover in a later episode) on a new approach to making a type theory extensional. The idea is to have equality types reduce, within the theory, to statements of extensional equality for the type of the values being equated.

Interjection: The Liquid Tensor Experiment Mar 02, 2023

I pause the chapter on extensionality in type theory to talk about something very exciting that I just learned about (though the project was completed Summer 2022): the so-called Liquid Tensor Experiment, to formalize a recent very difficult proof by a mathematician named Peter Scholze, in Lean. This is the first time in history, that I know of, when a theorem was formalized in a theorem prover, in order to resolve doubts of the mathematician who proved it. An amazing achievement. This episode tells the story, as I have understood it on line. The result apparently sparked this recent workshop.

Extensional Martin-Loef Type Theory Feb 03, 2023

In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection. This rule says that propositional equality implies definitional equality. Algorithmically, it would imply that the type checker should do arbitrary proof search during type checking, to see if two expressions are definitionally equal. This immediately gives us undecidability of type checking for the theory, at least as usually realized.

Begin chapter on extensionality Jan 24, 2023

This episode begins a new chapter on extensionality in type theory, where we seek to equate terms in different ways based on their types. The basic example is function extensionality, where we would like to equate functions from A to B if given equal inputs at type A, they produce equal outputs at type B. With this definition, quicksort and mergesort are equal, even though their codes are not syntactically equivalent. The episode begins by reviewing the distinction between definitional and propositional equality.
Also, I am still seeking your small donations ($5 or $10 would be awesome) to pay my podcast-hosting fees at Buzzsprout. To donate, click here, and then under "Gift details" select "Search for additional options" and then search for Computer Science. Select the Computer Science Development Fund, College of Liberal Arts and Sciences. Then add gift instructions saying that this is to support the Iowa Type Theory Commute podcast of Aaron Stump. Sorry it's that complicated.

Papers from Formal Methods for Blockchains 2021 Jan 01, 2023

In this episode, I talk about two papers from the 3rd International Workshop on Formal Methods for Blockchains, 2021. Also, I am continuing my request for your small donations ($5 or $10 would be awesome) to pay my podcast-hosting fees at Buzzsprout. To donate, click here, and then under "Gift details" select "Search for additional options" and then search for Computer Science. Select the Computer Science Development Fund, College of Liberal Arts and Sciences. Then add gift instructions saying that this is to support the Iowa Type Theory Commute podcast of Aaron Stump. Sorry it's that complicated.

Mi-Cho-Coq: Michelson formalized and applied, in Coq Dec 02, 2022

In this episode, I discuss this paper, "Mi-Cho-Coq, a Framework for Certifying
Tezos Smart Contracts", by Bernardo et al. The paper gives a nice and very clear introduction to the Michelson language, and a formalization of it in Coq. This is used to prove a correctness property about a Multisig contract.
I also kindly solicit your small donations ($5 or $10 would be awesome) to pay my podcast-hosting fees at Buzzsprout. To donate, click here, and then under "Gift details" select "Search for additional options" and then search for Computer Science. Select the Computer Science Development Fund, College of Liberal Arts and Sciences. Then add gift instructions saying that this is to support the Iowa Type Theory Commute podcast of Aaron Stump. Sorry it's that complicated.

Verification of Tezos smart contracts with K-Michelson Nov 10, 2022

In this episode (proudly wearing my "I am not an expert" hat), I discuss efforts by Runtime Verification to verify the Dexter2 defi smart contract, using their K-Michelson tool, which provides an executable description of the operational semantics of the Michelson language used for smart contracts on the Tezos blockchain.

Start of Season 4: Formal Methods for Blockchain Nov 07, 2022

I start off a new chapter (seventeen!) of the podcast, to talk about formal methods for blockchain systems. In the next few episodes, we will look at some verification efforts related to the Tezos blockchain.

Separation Logic II: recursive predicates Sep 15, 2022

I discuss separation logic basics some more, as presented in the seminal paper by John C. Reynolds. An important idea is describing data structure using separating conjunction and recursive predicates.

Separation Logic 1 Jul 24, 2022

I discuss separation logic, as presented in this seminal paper by the great John C. Reynolds. I did not go very far into the topic, so please expect a follow-up episode.

Let's talk about Rust Jul 09, 2022

In this episode, I talk briefly about Rust, which uses compile-time analysis to ensure that code is memory-safe (and also free of data races in concurrent code) without using a garbage collector. Fantastic! The language draws on but richly develops ideas on ownership that originated in academic research.

Region-Based Memory Management Jun 21, 2022

I discuss the idea of statically typed region-based memory management, proposed by Tofte and Talpin. The idea is to allow programmers to declare explicitly the region from which to satisfy individual allocation requests. Regions are created in a statically scoped way, so that after execution leaves the body of the region-creation construct, the entire region may be deallocated. Type inference is used to make sure that no dangling pointers are dereferenced (after the associated region is deallocated). This journal paper about the idea is not easy reading, but has a lot of good explanations in and around all the technicalities. Even better, I found, is this paper about region-based memory management in Cyclone. There are lots of intuitive explanations of the ideas, and not so much gory technicality.

Introduction to verified memory management Jun 04, 2022

In this episode, I start a new chapter (we are up to Chapter 16, here), about verifying safe manual management of memory. I have personally gotten pretty interested in this topic, having seen through some simple experiments with Haskell how much time can go into garbage collection for seemingly simple benchmarks. I also talk about why verifying memory-usage properties of programs is challenging in proof assistants.

More on Metamath May 20, 2022

I laud the Metamath proof checker and its excellent book. I am also looking for suggestions on what to discuss next, as I am ready to wrap up this chapter on proof assistants.

Metamath Apr 23, 2022

In this episode I share my initial impressions -- very positive! -- of the Metamath system. Metamath allows one to develop theorems from axioms which you state. Typing or other syntactic requirements of axioms or theorems are also expressed axiomatically. The system exhibits an elegant coherent vision for how such a tool should work, and was super easy to download and try out.

The Seventeen Provers of the World Apr 09, 2022

I discuss a book edited by Freek Wiedijk (pronounced "Frake Weedike"), which describes the solutions he received in response to a call for formalized proofs of the irrationality of the square root of 2. The book was published in 2006, and made an impression on me then. The provers we have discussed so far all have a solution in the book, except for Lean, which was created after that year. Happily, you can find a PDF of the book here, on Wiedijk's web site.

More on Lean Mar 12, 2022

I talk about my positive experience trying out the tools for Lean, specifically the 'lean' executable and lean-mode in emacs.

The Lean Prover Feb 27, 2022

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

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

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

I talk a bit more about the Agda proof assistant.

A look at Agda Jan 09, 2022

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

More reflections on Coq Dec 31, 2021

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

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

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

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

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

Introduction to Ordinal Analysis Nov 16, 2021

Ordinal analysis is an important branch of proof theory, which seeks to compare, quantitatively, the strengths of different proof systems. The quantities in question are ordinals, which extend the ordering character of natural numbers into the infinite. In this episode, I discuss these ideas a bit further, and also review a little the ordinals up to epsilon 0.

An analogy for multiplicative disjunction Nov 03, 2021

Listen in while I have an actual insight on air! After a week of head scratching, I figure out -- while chattering! -- what I hope is both a correct and intuitive example of multiplicative disjunction.

Linear conjunctions and disjunctions Oct 28, 2021

I explain the basic idea of multiplicative versus additive proof rules, and consider multiplicative conjunction (tensor), addition conjunction (&, "with"), additive disjunction -- but leaving multiplicative disjunction (par) for next time!

A taste of linear logic Oct 21, 2021

We discuss briefly the central ideas of linear logic, where by default assumptions must be used exactly once.

Structural rules, or the Curse of the Bound Variable Oct 12, 2021

In this episode I discuss the basic structural rules of weakening, contraction, and exchange, and speculate on their dark origin.

Why Cut Elimination is More Complicated than Normalization Oct 05, 2021

Cut elimination for sequent calculus is more involved that normalization of detours for natural deduction. There are more cases of cuts that must be transformed than correspond to detours (introductions followed by eliminations). In this episode, I explain why that is.

Introduction to Cut Elimination Sep 29, 2021

We saw in the last few episodes that proofs in natural deduction can be simplified by removing detours, which occur when an introduction inference is immediately followed by an elimination inference on the introduced formula. What corresponds to this for sequent calculus proofs? The answer is cut elimination. This episode describes the cut rule and what is meant by a cut-elimination procedure. We will talk more about such a procedure in the next episode.

Normalization of detours for implication inferences Sep 19, 2021

We talk about normalizing detours -- which are when an introduction inference is immediately followed by an elimination inference -- for the implication rules. Under Curry-Howard, this actually corresponds to beta-reduction, and could make the proof bigger (though less complex in a certain sense).

Normalization in natural deduction Sep 18, 2021

This episode explains the idea of normalization of proofs in natural deduction. We want to eliminate so-called detours in proofs, which occur when an introduction is immediately followed by an elimination.

A Brief Look at Sequent Calculus Sep 15, 2021

Sequent calculus is a different style in which proof systems can be formulated, where for each connective, we have a left rule for introducing it (in the conclusion of the rule) in the left part of a sequent G => D (i.e., in G), and similarly a right rule for introducing it in the right part (D). The beauty of sequent calculus is disjunction is handled without any departure from the general form for sequent calculus rules (unlike disjunction in natural deduction, as we discussed last time).

Natural deduction: or, the bad news! Sep 14, 2021

We discuss the problem of the or-elimination rule in natural deduction, which does not have the correct form for natural deduction inferences. It is a research problem to fix this!
Don't forget to get in touch with me if you want to do the mini-course over Zoom next month, on normalization.

Implication rules for natural deduction Sep 14, 2021

We discuss further inferences in natural deduction, in particular implication introduction and elimination.

Natural Deduction Sep 11, 2021

This episode begins the discussion of the style of proof known as Natural Deduction, invented by Gerhard Gentzen, a student of Hermann Weyl, himself a student of David Hilbert (sorry, I said incorrectly that Gentzen was Hilbert's own student). Each logical connective (like OR, AND, IMPLIES, etc.) has introduction rules that let you prove formulas built with that connective; and elimination rules that let you deduce consequences from a proven formula built with that connective.

Rules of proof, standard proof systems Sep 08, 2021

We continue our gradual entry into proof theory by talking about reflecting meta-logical reasoning into logical rules, and naming the three basic proof systems (Hilbert-style, natural deduction, and sequent calculus).
Advertising for the October 3-session Zoom mini-course on normalization continues. Email me if you are interested! This is just for ITTC listeners.
Finally, if you like the podcast and want to support it, would you consider a small ($5 or $10 is great) donation? This is not so much to cover the $12/month hosting fee at Buzzsprout but to get some kudos here at my institution, so people here know that I have a podcast [grin] and that listeners like it. To donate, go here, then choose "Colleges", then "College of Liberal Arts and Sciences", and then tick "Computer Science Development Fund". For "gift details", please leave "gift instructions" that say the gift is for Aaron Stump for the Iowa Type Theory Commute podcast. Then the money will get to the right place for me to use it for this. Thanks a lot in advance!

Different proof systems, distinguishing logical rules from domain axioms Sep 01, 2021

I highlight two basic points in this continuing warm-up to proof theory: there are different proof systems for the same logics, and it is customary to separate purely logical rules (dealing with propositional connectives and quantifiers, for example) from rules or axioms for some particular domain (like axioms about arithmetic, or whatever domain is of interest).

Introduction to Proof Theory (Start of Season 3) Aug 31, 2021

This is the start of Season 3 of the podcast. We are beginning with a new chapter (Chapter 14) on Proof Theory. This episode gives some basic introduction to the history and broad concerns of proof theory. There is even music, composed and played by yours truly, chez nous...

Modula-2 Jul 27, 2021

In this episode I discuss the paper "Modula-2 and Oberon" by Niklaus Wirth. Modula-2 introduced (it seems from the paper) the idea of having modules with explicit import and import lists -- something we saw at the start of our look at module systems with Haskell's module system. I note some interesting historical points raised by the paper.

Decomposing recursions using algebras Jul 12, 2021

Analogously to the decomposition of a datatype into a functor (which can be built from other functors to assemble a bigger language from smaller pieces of languages) and a single expression datatype with a sole constructor that builds an Expr from an F Expr (where F is the functor) -- analogously, a recursion can be decomposed into algebras and a fold function that applies the algebra throughout the datatype.

Reassembling datatypes from functors using a fixed-point Jul 10, 2021

Last episode we discussed how functors can describe a single level of a datatype. In this episode, we discuss how to put these functors back together into a datatype, using disjoint unions of functors and a fixed-point datatype. The latter expresses the idea that inductive data is built in any finite number of layers, where each layer is described by the functor for the datatype.

Decomposing datatypes into functors Jul 03, 2021

This episode continues the discussion of Swierstra's paper "Datatypes à la Carte", explaining how we can decompose a datatype into the application of a fixed-point type constructor and then a functor. The functor itself can be assembled from other functors for pieces of the datatype. This makes modular datatypes possible.

Modular datatypes: introducing Swierstra's paper "Datatypes à la Carte" Jun 24, 2021

In a really wonderful paper of some few years back, Swierstra introduced the idea of modular datatypes using ideas from universal algebra. Modular datatypes allow one to assemble a bigger datatype from component datatypes, and combine functions written on the component datatypes in a modular way. In this episode I introduce the paper and the problem (dubbed the expression problem by Phil Wadler) it is trying to solve. Modular datatypes are a different form of modularity that I would like to consider in the context of the discussion of module systems we have been engaged in now for a while in Chapter 13 of the podcast.

Modules for Mathematical Theories (MMT) Jun 08, 2021

In a 2013 journal article titled "A Scalable Module System", Florian Rabe and Michael Kohlhase propose a module system called MMT (Modules for Mathematical Theories) for structuring mathematical knowledge. The paper has a very interesting general discussion of module systems, from programming languages but also other areas like algebraic specification and theorem proving. The system is based on a rather small set of concepts which subsume those of, for example, Standard ML's module system. Thought-provoking!

Some thoughts on module systems so far May 18, 2021

I look back at the module systems we considered so far (Haskell's, Standard ML's, and Agda's), and consider a few points that are on my mind about these. I also mention a few other languages' module systems (Clojure, Java 9). I also ponder names and namespace management.

A look at Agda's module system May 12, 2021

Agda's module system (beautifully described here) could be seen as intermediate between Haskell's and Standard ML's. It supports nested parametrized modules with information hiding, but does not go all the way to higher-order functors (as in Standard ML).

Standard ML: the Newmar King-Aire of module systems May 10, 2021

SML has arguably the most complicated/powerful module system of any existing programming language. It is a luxury RV to Haskell's camper van. I take a high-level look, following a very nice paper by Xavier Leroy, titled "A modular module system".

A look at Haskell's module system Apr 26, 2021

I briefly survey the main features of Haskell's module system, and reflect a bit on its design.

Let's talk about modules! Apr 20, 2021

I start Chapter 13 (in Season 2) of the podcast, on module systems. Almost all programming languages I know include some kind of scheme for modules, packages, namespaces, or something like this. I discuss the high-level ideas of namespace management and type abstraction, two main use cases for module systems. Subsequent episodes will discuss module systems (from papers or documentation) of various languages.

Church-style Typing and Intersection Types: Glimpses of Benjamin Pierce's Dissertation Apr 12, 2021

I was reading Benjamin Pierce's dissertation, and learning some intriguing things about intersection types in the context of Church-style typing. I summarize the parts of this I comprehended so far.

Intersections and Unions in Practice; Failure of Type Preservation with Unions Mar 22, 2021

I discuss the perhaps surprising fact that union and intersection types are quite actively used and promoted for languages like TypeScript, also OO languages like Scala. I also try to explain briefly a counterexample to type preservation with union types, which you can find at the start of Section 2 of Barbanera and Dezani-Ciancaglini's paper "Intersection and Union Types: Syntax and Semantics", where it is attributed to Benjamin Pierce.

Normal terms are typable with intersection types Mar 05, 2021

I sketch the argument that pure lambda terms in normal form are typable using intersection types. This completes the argument started in the previous episode, that intersection types are complete for normalizing terms: normal forms are typable, and typing is preserved by beta-expansion. Hence any normalizing term is typable (since it reduces to a normal form by definition, and from this normal form we can walk typing back to the term).

Intersection Types Preserved Under Beta-Expansion Feb 15, 2021

Type systems usually have the type preservation property: if a typable term beta-reduces, then the resulting term is still typable. So typing is closed under beta-reduction. With intersection typing, typing is also closed under beta-expansion, which is a critical step in showing that intersection typing is complete for normalizing terms: any normalizing term can be typed with intersection types (and simple function types).

Introduction to Intersection Types Feb 08, 2021

In a type system with intersection types, a term t that has type A and also has type B can be assigned the type 'A intersect B'. This episode begins Chapter 12 of the podcast on intersection types.

Deriving disjointness of constructor ranges in RelTT Feb 02, 2021

Responding to an email question from a listener, I explain how to derive a form of inconsistency from the assumption that True is related to False at type Bool.

Software Design and Intrinsic Identity Jan 20, 2021

I muse about the hopeless prospect of a single intrinsic conceptual decomposition of a problem domain in software engineering, and relate this to the idea of intrinsic identity we discussed recently for Relational Type Theory.

Identity Inclusion in Relational Type Theory Jan 18, 2021

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"), RelTT instead has a refinement of this called Identity Inclusion. Instead of saying that the interpretation of every closed type is the identity relation (Identity Extension), the Identity Inclusion lemma identifies certain types whose relational meaning is included in the identity relation, and certain types which include the identity relation. So there are two subset relations, going in opposite directions. The two classes of types are first, the ones where all quantifiers occur only positively, and second, where they occur only negatively. Using Identity Inclusion, we can derive transitivity for forall-positive types, which is needed to derive induction following the natural generalization of the scheme in Wadler's paper (last episode).

On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler Jan 18, 2021

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 type for Church-encoded natural numbers implies induction. RelTT uses a generalization of these ideas to derive induction for any positive type family.

Equivalence of inductive and parametric naturals in RelTT Dec 28, 2020

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.

Examples in Relational Type Theory Dec 23, 2020

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

The Semantics of Relational Types Dec 22, 2020

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

The Types of Relational Type Theory Dec 14, 2020

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.

Introducing Relational Type Theory Dec 14, 2020

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

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

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

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

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

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

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

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

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

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.

Introduction to Logical Relations Aug 16, 2020

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 Season 2, as the fall academic year is just beginning here in Iowa.

Lamping's abstract algorithm Jul 25, 2020

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 one duplicator down the variable port, and another down the body port. When they meet, they cancel each other and the duplication is done. But duplication can get paused waiting for a value to come in on a wire from outside the lambda abstraction. This can lead to a situation where some other duplication needs to duplicate a lambda graph containing frozen duplicators. Then we have to decide, when two duplicators meet, should they cancel each other (signalling the end of a duplication on one level), or should one duplicate the duplicators (for an outer duplication of some lambda graph containing frozen duplicators). The abstract algorithm leaves this choice undetermined. The hairy versions of the algorithm add complex additional machinery to keep track of these levels of duplication to resolve that nondeterminism.

Examples showing non-optimality of Haskell Jul 14, 2020

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 major help with these.

Lambda graphs with duplicators and start of Lamping's abstract algorithm Jul 03, 2020

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' abstract algorithm for optimal beta-reduction, in particular how we need to push duplicators inside lambda abstractions to initiate a lazy duplication.

Duplicating redexes as the central problem of optimal reduction Jun 20, 2020

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 episode the central issue with doing that, namely copying redexes and copying applications which could turn into redexes following other beta reductions. The high-level idea of the proposed solution is also discussed, namely lazy graph duplication.

Introduction to optimal beta reduction Jun 16, 2020

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 try to duplicate it incrementally.

Lexicographic termination Jun 02, 2020

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 does (and then the B component can increase unboundedly) or else the A component stays the same and the B component decreases. Connections with nested recursion and ordinals discussed.

Mendler-style iteration May 18, 2020

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 coding against a certain interface that features an abstract type R, which abstracts the datatype over which we are recursing; and a function from R to the result type of the recursion. Subdata of the input data are available at type R only, not at the original datatype. This allows us to make explicit recursive calls, but only on subdata.

Well-founded recursion May 18, 2020

Well-founded recursion is a technique to turn recursion which decreases along a well-founded ordering into a structural recursion.

Compositional termination checking with sized types Mar 30, 2020

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 the data as input to the recursion. Since the method is type-based, it is compositional: we can break out helper functions from a recursive function and not upset the termination checker. A readable and interesting tutorial on the subject is here.

Noncompositionality of syntactic structural-recursion checks Mar 19, 2020

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 may pass the syntactic termination check, but abstracting part of it out into a helper function may result in code which no longer passes the check. So we need a compositional termination check, which will be discussed in subsequent episodes.

Structural termination Mar 17, 2020

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 Coq (called the Calculus of Constructions). Considering the most basic form of termination checking, which is checking syntactically that recursive calls are only made on subdata of the data input to the recursive function.

Proving Confluence for Untyped Lambda Calculus II Mar 13, 2020

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!

Proving Confluence for Untyped Lambda Calculus I Mar 13, 2020

Start of discussion on how to prove confluence for untyped lambda calculus. Also some discussion about the research community interested in confluence.

Confluence, and its use for conversion checking Mar 11, 2020

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 t1 and t2 both reduce in a finite number of steps. The use of confluence for ensuring completeness of the conversion-checking algorithm that tests conversion of t1 and t2 by normalizing both terms and checking for alpha-equivalence (or maybe alpha,eta-equivalence).

Normalization and logical consistency Mar 09, 2020

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 eliminated from proofs (this is normalization) and that the resulting proof still proves the same theorem (this is type preservation). I mention an alternative I use for Cedille, which is to use a realizability semantics (often used for normalization proofs) directly to prove consistency.

Normalization in type theory: where it is needed, and where not Mar 06, 2020

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. Traditionally, type theorists have also desired normalization or even termination (every term reaches a normal form no matter what reduction sequence is explored in a nondeterministic operational semantics) for conversion checking. This is the process of confirming that types are equivalent during type checking, which, due to dependent types, can require checking program equivalence. The latter is usually restricted to just beta-equivalence (where beta-reduction is substitution of argument for input variable when applying a function), because richer notions of program equivalence are usually undecidable. I have a mini-rant in this episode explaining why this usual requirement of normalization for conversion checking is not sensible.
Also I note that you can find the episodes of the podcast organized by chapter on my web page.

Introduction to normalization Mar 05, 2020

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 type theory, the need for normalization due to Curry-Howard and due to conversion checking.

Proving type safety; upcoming metatheoretic properties Mar 04, 2020

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 system is correct. Looking ahead, this episode also talks about the different between normalization and termination when your language is nondeterministic, and the property of confluence.

The progress property and the problem of axioms in type theory Mar 03, 2020

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 can lead to a failure of progress.

Introduction to type safety Mar 02, 2020

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 preservation says that if a program expression e has some type T, then running e a bit will give a result that still has type T (and type preservation would apply again to that result, to preserve the type T indefinitely along the execution of e). Progress says that well-typed expressions cannot get stuck computationally: they cannot reduce to a form where the operational semantics is then undefined. This is how we model the idea that the type system is preventing certain kinds of failures: make those failures correspond to undefined behavior.

Introduction to metatheory Feb 28, 2020

Metatheory is concerned with proving properties about theories, in this case type theories or programming languages.

Definition of the Mendler encoding Feb 26, 2020

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 recursive calls (rather than in the Church encoding, where the data present the programmer's combining function with the results of all possible recursive calls on immediate subdata).

The Mendler encoding and the problem of explicit recursion Feb 25, 2020

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 subdata. Using a technique due to Mendler, an encoding is possible where recursions are explicitly made by the combining functions given to the data.

The Scott encoding Feb 24, 2020

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 the immediate subdata of the data.

More on the Parigot encoding Feb 21, 2020

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.

Introduction to the Parigot encoding Feb 18, 2020

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.

Church-encoding natural numbers Feb 17, 2020

What is fold-right for a natural number? How do we define addition with this? The problem of inefficient predecessor.

Church encoding of lists Feb 14, 2020

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 Feb 14, 2020

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 is forall X. X -> X -> X.

Introduction to Church encoding Feb 11, 2020

The Church encoding represents data as their own fold-right functions

Functional encodings turning the world inside out Feb 11, 2020

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 Feb 07, 2020

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 Feb 07, 2020

A lambda encoding is some way of representing data as functions (lambda abstractions). Some motivations for this for computer-checked proofs and type theory.

Adding a top type and allowing non-normalizing terms Feb 04, 2020

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 Feb 04, 2020

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 Jan 30, 2020

In Curry-style typing annotations -- for example, the types of bound variables -- are erased, and not truly (semantically) part of the term. In Church-style, they are intrinsic to the term and are truly there. Discussion of some of the practicalities of Curry-style typing, in particular type annotations versus proving typings.

More on Computation First, and Basic Idea of Realizability Jan 29, 2020

Types are specifications whose semantics is explained in terms of computation, which is thus conceptually prior. Realizability is a way of explaining the semantics of types.

Types should be erased for executing and reasoning about programs Jan 29, 2020

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 with dependent types, for example, where we can reason about program execution statically).

Why go beyond GADTs? Jan 24, 2020

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 podcast) or not?

GADTs for programming with representations of types Jan 22, 2020

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 consumes a number of inputs that is controlled by an argument to the function.

Using GADTs for typed subsetting of your language Jan 20, 2020

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, where a is a type of the language (say this language is Haskell). Values of types Expr a are the abstract syntax trees of expressions of type a from your host language. This is just a special case of embedding a typed language into your host language: in this case the typed language is a subset of your host language.

Example of programming with indexed types: binary search trees Jan 16, 2020

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 enforce the binary search tree property using an indexed type bst l u, where l is a lower bound and u an upper bound on the data stored in the tree.

Programming with indexed types using singletons Jan 16, 2020

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 data value of type Nat n is a copy of n, but living in the syntactic category of program expressions. This allows programs to operate on a proxy for n. Singletons library in Haskell mentioned.

Limitations of indexed types that are not truly dependent Jan 14, 2020

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 work around these.

Programming with Indexed Types Jan 13, 2020

Indexed datatypes like vectors, where the indices come from a different syntactic category than program expressions.

Program Termination and the Curry-Howard Isomorphism Jan 10, 2020

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 type. Under Curry-Howard this means any formula is provable, which is one way to define inconsistency. (And logics have to be consistent to be useful.)

Why Curry-Howard for classical proofs is a bad idea for programming Jan 06, 2020

If you have dependent types, classical reasoning, and the Curry-Howard isomorphism, you can write programs that look like they are invoking oracles for undecidable problems -- but they are not, and this is confusing.

Curry-Howard for classical logic Jan 06, 2020

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 Formulae-as-Types Notion of Control</a> by Timothy Griffin. I discuss how backtracking implements the law of excluded middle.

Dependent types and design by contract Jan 03, 2020

Dependent types are discussed, particularly as used for expressing pre- and post-conditions of functions.

Indexed types and Curry-Howard for first-order quantifiers Jan 03, 2020

I follow up on some comments I made about Curry-Howard for first-order quantifiers in the previous episode. Sheard's Omega language also mentioned (see links on <a href = "http://web.cecs.pdx.edu/~sheard/">his web page</a>). First-order quantifications turn into indexed types where the indices are not program expressions but come from another syntactic domain.

The Curry-Howard Isomorphism for Propositional Logic Jan 02, 2020

Discussion of the Curry-Howard isomorphism for the connectives of propositional logic (AND, OR, NOT, FALSE, IMPLIES). Initial consideration of Curry-Howard for first-order and higher-order logic. Dependent types.

The Curry-Howard Isomorphism for Induction Dec 31, 2019

In which I discover why the domino analogy for explaining induction always bothered me!

Constructive proofs as programs Dec 21, 2019

We consider the basic idea of the Curry-Howard isomorphism, that constructive proofs are essentially programs, and vice versa. Several simple examples. Why the law of excluded middle is not a legal constructive proof.

Introduction to the Curry-Howard Isomorphism Dec 20, 2019

The basic idea of the Curry-Howard isomorphism, and its connection to the contents of Chapters 1 and 2. Constructive proof. A famous nonconstructive proof.

Functors and catamorphisms Dec 20, 2019

More about the structured recusion scheme known as the catamorphism. Basic idea of functors.

Structured Recursion Schemes for Point-Free Recursion Dec 18, 2019

Review of basic application of category theory for functional programming. Recursion schemes are combinators that let you write point-free recursions.

More on point-free programming and category theory Dec 17, 2019

A few very basic ideas of categories and combinators. Also, the problem of understanding very concise code.

Point-free programming and category theory Dec 17, 2019

Relation of point-free functional programming to category theory.

Concise code through point-free programming Dec 13, 2019

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 functions on inputs explicitly.

More on FP and concise code Dec 12, 2019

Discussion of datatypes for tree-like data structures in functional languages. Usefulness of these for processing structured linguistic artifacts, where the structure is represented by the tree structure.

Functional Programming and Concise Code: Type Inference Dec 12, 2019

Start of discussion of some of technology and culture that lead to more concise code in functional programming languages. Type inference to avoid writing types for local and input variables. Some basics of static and dynamic typing.

Introduction to Functional Programming Dec 11, 2019

Introduction to the basic idea of functional programming. Three kinds are discussed: functional programming with mutable state, pure functional programming (where there is no implicit state), and strong functional programming (which is pure functional programming where every function is statically required to terminate).

Software Engineering Considerations for Formal Methods Dec 01, 2019

Discussion of some practicalities of applying formal methods to software. Ideally we are seeking techniques that can be applied with increasing effort to yield increasingly strong results. Also, introduction to functional programming.

Power of Computer-Checked Proofs for Software Nov 30, 2019

Continuing pessimistic discussion about the purpose of formal methods for Computer Science. But then counter arguments about the value of absolutely correct software.

Technical reasons for lack of adoption of computer-checked proofs Nov 28, 2019

Discussion of a technical reason for lack of adoption of computer-checked proofs for mathematics, namely the level of detail in the proof. Proof assistants require too much detail in proofs to allow mathematicians to carry over their elegant art of expressing just the right amount of information to convey the idea of the proof to a mathematically competent reader. For Computer Science, a problem of adoption is that proofs are computationally useless (generally).

Why Computer-Checked Proofs are Not Used More in Mathematics Nov 27, 2019

Some discussion of why computer-checked proofs have not been adopted more in mathematics. The psychology of telling mathematicians their time-honored method of investigation is inadequate and they need computer-checked proofs. Computer-checked proofs and certainty.

Computer-Checked Proofs in American Research Nov 26, 2019

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 in the late 1990s and early 2000s that helped raise awareness in the US of computer-checked proofs: proof-carrying code, the POPLmark challenge.

Computer-checked proofs about software Nov 23, 2019

Computer-checked proofs can ensure properties of software. Discussion of several aspects of this idea.

More on Computer-Checked Proofs Nov 22, 2019

Further discussion of computer-checked proofs, including the example of the proof by Hales and his collaborators of the Kepler Conjecture. Automath also mentioned. DAO hack on Ethereum and the interest in cryptocurrency community in computer-checked proofs.

Computer-checked proofs Nov 21, 2019

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.

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected