Iowa Type Theory Commute

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

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

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.

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.

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

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

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.

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

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.  

I talk a bit more about the Agda proof assistant.

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

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.

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.

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.

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

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, bu...

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.

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.

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!

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

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

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.

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

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.