Concoqtion: Indexed types now!

programming languages community is vigorously pursuing ways to incorporate F!-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.

• Type: Conference
• Year: 2007
• Where: PEPM
• Authors: Emir Pasalic, Jeremy G. Siek, Seth Fogarty, Walid Taha
• Keywords: Concoqtion, Dependant Types, Indexed Types, Theorem Proving, Type Systems, Type Theory