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
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.
- Download distribution
(01/05/2007). This is prototype version has been tested on Linux and
Mac OS X 10.4.
- A brief introduction
including installation instructions is now available
- A talk at
- A more detailed introduction to the design goals can be found in the PEPM 2007 paper
Indexed types now!
- Our approach to type inference is described in the technical report
Mixing Indexed Types and Hindley-Milner Type Inference (07/28/2006).
- Concoqtion is discussed on the
- Please send bug reports to the
- Software release history:
- 01/05/2007: C-07 version is first official public release.
- 10/31/2006: C-06 version supports staging, compliant with OCaml 3.08 and MetaOCaml 027.
- Related Systems:
Harper and Licata's extension to DML,
Lightwight dependent types,
First Class Phantom Types,
GADTs for Object-oriented languages,