They recently released the Concoqtion, which is MetaOCaml integrated with the Coq theorem prover:
"Concoqtion is an extension to MetaOCaml with indexed types. [...] Only a small number of extensions to the term and type language are needed to give the user full access to the powerful Coq proof checker at the level of types. [...] Because Coq is one of the most expressive checkers available, any fact that can be proved in Coq can be used to give more refined types to programs. Because Coq propositions can be viewed as types, Concoqtion provides a natural way to incorporate formal verification techniques into programming practice." http://www.metaocaml.org/concoqtion/ _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
