Home | Search | Help  
Home Page Università di Genova

Seminar Details

Date 16-4-2003
Time 15:00
Room/Location 214
Title A calculus of call-by-value mixin modules
Speaker Tom Hirschowitz
Affiliation INRIA
Link http://cristal.inria.fr/~hirschow/
Abstract The ML module system provides powerful parameterization facilities, but lacks the ability to split mutually recursive definitions across modules, and does not provide enough facilities for incremental programming. A promising approach to solve these issues is mixin modules. Ancona and Zucca [1] and Wells and Vestergaard [3] have studied mixin modules calculi in a call-by-name setting. However, the straightforward way to adapt it to ML fails, because arbitrary recursive definitions may appear at any time, which ML does not support. Hirschowitz and Leroy [2] have formalized a language of call-by-value mixin modules, whose semantics is given by type-directed translation down to a call-by-value lambda-calculus extended with a non-standard "let rec" construct. This presentation makes equational reasoning difficult and prevents mixin modules to be first class entities in the language. We present MM, a call-by-value calculus of mixin modules, with an untyped reduction semantics. A type system is formalized and proved sound. [1] D. Ancona and E. Zucca, A calculus of module systems, JFP 2002. [2] T. Hirschowitz and X. Leroy, Mixin modules in a call-by-value setting, ESOP 2002. [3] J.B. Wells and R. Vestergaard, Equational reasoning for linking with first-class primitive modules, ESOP 2000.
Back to Seminars