Concoqtion
- 15 January 2007
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 112-121
- https://doi.org/10.1145/1244381.1244400
Abstract
Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporateF!-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming lan- guages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type in- ference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the com- piler; and yields a language comparable in notation to the leading proposals. The resulting language provides unlimited expressive- ness in the type system while maintaining decidability. Further- more, 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.Keywords
This publication has 18 references indexed in Scilit:
- A constraint-based approach to guarded algebraic data typesACM Transactions on Programming Languages and Systems, 2007
- Formal certification of a compiler back-end orPublished by Association for Computing Machinery (ACM) ,2006
- Generalized algebraic data types and object-oriented programmingPublished by Association for Computing Machinery (ACM) ,2005
- Combining programming with theorem provingPublished by Association for Computing Machinery (ACM) ,2005
- Languages of the futureACM SIGPLAN Notices, 2004
- Inductive Families Need Not Store Their IndicesPublished by Springer Nature ,2004
- DSL Implementation in MetaOCaml, Template Haskell, and C++Published by Springer Nature ,2004
- Implementing typeful program transformationsPublished by Association for Computing Machinery (ACM) ,2003
- A type system for certified binariesACM SIGPLAN Notices, 2002
- Tag Elimination and Jones-OptimalityPublished by Springer Nature ,2001