|
(via Frank's PLT Online)
Morten Heine B. Sørenson and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism.
Warning: This set of lecture notes is long!
This is a very good introduction to an important idea: The Curry-Howard Isomorphism between systems of formal logic and computational type systems.
The isomorphism has many aspects, even at the syntactic level: formuals correspond to types, proofs correspond to terms, provability corresponds inhabitation, proof normalization corresponds to term reduction etc. (from the preface)
The text is fairly self contained, and starts from an explanation of the Lambda Calculus (LC) and the typed lambda calculus. It then goes on to talk about intuitionistic logic. Only after this preparation the Curry-Howard isomorphism is explored.
The text includes exercises.
Posted to theory by Ehud Lamm on 12/27/01; 11:27:49 AM
|
Lectures on the Curry-Howard Isomorphism
