Chapter 3, addendum 2: A pedagogical introduction to Curry-Howard correspondence for programmers

Title:

Introduction to the Curry-Howard correspondence: The logic of types in functional programming languages

Contents:

The commonality of type constructions in functional programming languages: Scala, OCaml, Haskell
Defining the propositions that correspond to types
What are "sequents" and how they are used to describe logical inference from premises
How logical derivations correspond to expressions in the programming language; how to convert one to the other and back
What is the "logic of types" defined by the common type constructions in the functional programming languages: it is the intuitionistic propositional logic (IPL)
Examples that contrast the IPL with the classical Boolean logic
Example of using Gentzen's calculus LJ to search for a proof
The advantage of the Vorobieff-Hudelmaier-Dyckhoff's calculus LJT over Gentzen's calculus LJ, and why people are using LJT for proof search
Example of what mathematicians mean when they say "it is trivial"
How to transform proofs back to code: proof transformer functions that correspond to derivation rules in LJ/LJT
Example of deriving code automatically from a proof of a sequent
How to use the "arithmetical Curry-Howard correspondence" to decide which types are equivalent
What are polynomial data types and exponential-polynomial data types
Summary: What are the practical uses of the CH correspondence
Limitations of the propositional logic: what it can and cannot do
Using the CH correspondence as a guide in programming language design

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/curryhoward-2018-tutorial.pdf