Tag : djinn

Even if your are a beginner in functional programming, you have probably heard of the program-as-proof correspondence, also known as the Curry-Howard isomorphism. It is a bridge between the world of logic and the world of computation. A type is a specification and a program is a proof of that type. Typechecking is just checking the proof. Types can be used to specify lots of constraints about your programs. With sophisticated type systems like the ones in [Ocaml](http://caml.inria.fr/ocaml/index.fr.html) and [Haskell](http://haskell.org/haskellwiki/Haskell) you can really do wonderful stuff. But, those type systems are not powerful enough. We may dream of extracting a program from its specification. But, for that we need to be able to express very rich specifications. It is possible with the calculus of constructions which is the type system implemented in [Coq](http://coq.inria.fr/).