Iowa Type Theory Commute Aaron Stump

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

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

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.

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. 

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

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.