Explaining the Curry-Howard correspondence for practical programmers. With code examples in Scala

This tutorial is a significantly shortened and revised version of my previous tutorials on the Curry-Howard correspondence. This tutorial is aimed at software engineers familiar with Scala or with similar functional programming languages (OCaml, Haskell).

Contents:

How CH correspondence helps write code by inferring code from type signatures

How to define a set of logical rules that determine rigorously whether a type signature can be implemented

Correspondence between types and logical propositions: what are "CH-propositions"

How code snippets determine logical relations between propositions

Limiting the available code snippets: what is "fully parametric" code

What are "sequents" and why they represent types of code expressions

Finding full set of logical rules for deriving statements about implementable types: the "constructive propositional logic"

How a proof in the logic corresponds to the code of a function, and vice versa: solved example

How the constructive logic is different from Boolean logic: examples

Why the logical rules need to be reformulated in order to obtain a decision algorithm

Gentzen's LJ algorithm: solved example

How the LJT algorithm removes infinite loops from the LJ algorithm

How to infer code from types using "proof transformers" with the LJ algorithm: solved example

Use cases for the `curryhoward` library in Scala

[HPGumm]

This is an excellent tutorial. Thank You.

[sassanf]

I didn't quite get the 0 |- CH(A=>B). Shouldn't it have been (CH(A) |- CH(B)) |- CH(A=>B)?