| Abstract
|
<p>Almost twenty years after the pio … <p>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.</p>-typed domain-specific language.</p>
|
| Author
|
Seth Fogarty +
, Emir Pasalic +
, Jeremy Siek +
, Walid Taha +
|
| Conference
|
PEPM'07. 2007 ACM SIGPLAN Workshop Partial Evaluation and Semantics-Based Program Manipulation, Nice, France, January 15-16
|
| DOI
|
http://dx.doi.org/10.1145/1244381.1244400 +
|
| Diva
|
http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:588262
|
| EndPage
|
121 +
|
| HostPublication
|
PEPM 2007 : proceedings of the Workshop on Partial Evaluation and Program Manipulation : Nice, France, January 15-16, 2007 +
|
| PublicationType
|
Conference Paper +
|
| Publisher
|
ACM Press +
|
| StartPage
|
112 +
|
| Title
|
Concoqtion : Indexed Types Now! +
|
| Year
|
2007 +
|
| Has queryThis property is a special property in this wiki.
|
Publications:Concoqtion : Indexed Types Now! +
, Publications:Concoqtion : Indexed Types Now! +
, Publications:Concoqtion : Indexed Types Now! +
, Publications:Concoqtion : Indexed Types Now! +
, Publications:Concoqtion : Indexed Types Now! +
, Publications:Concoqtion : Indexed Types Now! +
, Publications:Concoqtion : Indexed Types Now! +
, Publications:Concoqtion : Indexed Types Now! +
, Publications:Concoqtion : Indexed Types Now! +
, Publications:Concoqtion : Indexed Types Now! +
|
| Categories |
Publication +
|
| Modification dateThis property is a special property in this wiki.
|
26 June 2014 03:44:51 +
|
