Lectures on the Curry-Howard Isomorphism
by Morten Heine B. Sorensen, Pawel Urzyczyn
Publisher: Elsevier Science 2006
ISBN/ASIN: 0444520775
Number of pages: 273
Description:
The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic.
Download or read it online for free here:
Download link
(1.3MB, PDF)
Similar books
Categories, Types, and Structuresby Andrea Asperti, Giuseppe Longo - MIT Press
Here is an introduction to category theory for the working computer scientist. It is a self-contained introduction to general category theory and the mathematical structures that constitute the theoretical background.
(21492 views)
Formal Languagesby Keijo Ruohonen - Tampere University of Technology
In these notes the classical Chomskian formal language theory is fairly fully dealt with, omitting however much of automata constructs and computability issues. Surveys of Lindenmayer system theory and the mathematical theory of codes are given.
(11296 views)
Concrete Semantics: With Isabelle/HOLby Tobias Nipkow, Gerwin Klein - Springer
The book teaches the reader the art of precise logical reasoning and the practical use of a proof assistant as a tool for formal proofs about computer science artefacts. All the mathematics is formalised in Isabelle and much of it is executable.
(8917 views)
The Theory of Languages and Computationby Jean Gallier, Andrew Hicks - University of Pennsylvania
From the table of contents: Automata; Formal Languages (A Grammar for Parsing English, Context-Free Grammars, Derivations and Context-Free Languages, Normal Forms for Context-Free Grammars, Chomsky Normal Form, ...); Computability; Current Topics.
(11330 views)