Logo

Lectures on the Curry-Howard Isomorphism

Large book cover: Lectures on the Curry-Howard Isomorphism

Lectures on the Curry-Howard Isomorphism
by

Publisher: Elsevier Science
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

Book cover: The Z Notation: A Reference ManualThe Z Notation: A Reference Manual
by - Prentice Hall
The standard Z notation for specifying and designing software has evolved over the best part of a decade. This an informal but rigorous reference manual is written with the everyday needs of readers and writers of Z specifications in mind.
(12970 views)
Book cover: Computational Category TheoryComputational Category Theory
by
The book is a bridge-building exercise between computer programming and category theory. Basic constructions of category theory are expressed as computer programs. It is a first attempt at connecting the abstract mathematics with concrete programs.
(20244 views)
Book cover: The Theory of Languages and ComputationThe Theory of Languages and Computation
by - 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.
(10077 views)
Book cover: Semantics With Applications: A Formal IntroductionSemantics With Applications: A Formal Introduction
by - John Wiley & Sons
The book covers the foundations of structural operational semantics and natural semantics. It shows how to describe the semantics of declarative as well as imperative language constructs and will also touch upon non-sequential constructs.
(14623 views)