go to start Jannis Grimm
|home |print view |recent changes |changed December 21, 2015 |
exact
|You are 54.198.3.15 <- set your identity!

Sections: HS15 | Abstract |

HS15 ^

Abstract ^

Curry-Howard Isomorphism allows to map the world of intuitionistic logic to types from the world of programming languages and vice versa. This allows to validate mathematical proofs with a compiler. This paper explains the main principles behind Curry-Howard Isomorphism simple and down-to-earth with examples in Haskell. Theorems, Nontheorems, Implication, Conjunction, Disjunction and Negation are explained from both views, the world of intuistionistic logic and the world of programming languages. Both intuitionistic logic and reading Haskell syntax is explained, the required previous knowledge is reduced to a minimum and consists of classic logic and general knowledge of programming languages and types.


|home |print view |recent changes |changed December 21, 2015 |
exact
|You are 54.198.3.15 <- set your identity!

Jannis Grimm
go to start