Concoqtion

Concoqtion is an extension to MetaOCaml with indexed types. Indexed types are a powerful tool that allows the programmer to express nested polymorphism as well as complex functional dependencies at the level of 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. With these extensions, datatypes can be defined that reflect the size of a list or a vector in its type. An append function on sized lists can be given a type that reflects the way it acts on the size of lists. Using MetaOCaml staging constructs, it is possible to express tagless staged interpreters in Concoqtion.

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.