alpheccar's blog - tag djinn http://www.alpheccar.org en 40 science and freedom http://www.alpheccar.org alpheccar's blog - tag djinn http://www.alpheccar.org/images/avatar.jpg Djinn, Coq, Monad and a bit of Haskell 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/).

Read More...

]]> Thu, 24 May 2007 14:18:57 -0400 urn:uuid:65 webmaster@alpheccar.org http://www.alpheccar.org/en/posts/show/70 http://www.alpheccar.org/en/posts/show/70#comments haskell ocaml coq djinn