Sciweavers

POPL
1990
ACM

Higher-Order Modules and the Phase Distinction

13 years 7 months ago
Higher-Order Modules and the Phase Distinction
Typed -calculus is an important tool in programming language research because it provides an extensible framework for studying language features both in isolation and in their relation to each other. In earlier work we introduced a predicative function calculus, XML, for modeling several aspects of the Standard ML type system. Following MacQueen, our study focused on the use of dependent types to represent the modularity constructs of Standard ML. In addition to shedding some light on the trade-offs between language features, our analysis suggested that the first-order modules system of ML could be naturally extended to higher orders. However, whereas ML maintains a clear distinction between compile-time and run-time in both its implementation and formal semantics, the XML calculus blurs this distinction. Since static type checking is, in our view, essential to the practical utility of ML, we introduce a refinement of the XML calculus for which type checking is decidable at compile ti...
Robert Harper, John C. Mitchell, Eugenio Moggi
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1990
Where POPL
Authors Robert Harper, John C. Mitchell, Eugenio Moggi
Comments (0)