Publications:Concoqtion : Indexed Types Now!
From CERES
| Title | Concoqtion : Indexed Types Now! |
|---|---|
| Author | Seth Fogarty and Emir Pasalic and Jeremy Siek and Walid Taha |
| Year | 2007 |
| PublicationType | Conference Paper |
| Journal | |
| HostPublication | PEPM 2007 : proceedings of the Workshop on Partial Evaluation and Program Manipulation : Nice, France, January 15-16, 2007 |
| DOI | http://dx.doi.org/10.1145/1244381.1244400 |
| Conference | PEPM'07. 2007 ACM SIGPLAN Workshop Partial Evaluation and Semantics-Based Program Manipulation, Nice, France, January 15-16 |
| Diva url | http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:588262 |
| Abstract | Almost twenty years after the pioneering efforts of Cardelli, the 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. |
