A Church-Style Intermediate Language for MLF

Didier Rémy 1 Boris Yakobowski 2
2 LSL - Laboratoire Sûreté des Logiciels
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
Abstract : MLF is a type system that seamlessly merges ML-style implicit butsecond-class polymorphism with System-F explicit first-classpolymorphism. We present xMLF, a Church-style version of MLF with fulltype information that can easily be maintained during reduction. Allparameters of functions are explicitly typed and both type abstractionand type instantiation are explicit. However, type instantiation in xMLFis more general than type application in System F. We equip xMLF with asmall-step reduction semantics that allows reduction in any context, andshow that this relation is confluent and type preserving. We also showthat both subject reduction and progress hold for weak-reductionstrategies, including call-by-value with the value-restriction. Weexhibit a type preserving encoding of MLF into xMLF, which shows thatxMLF can be used as the internal language for MLF after type inference,and also ensures type soundness for the most expressive variant of MLF.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2012, 435, pp.77--105. 〈http://dx.doi.org/10.1016/j.tcs.2012.02.026〉. 〈10.1016/j.tcs.2012.02.026〉
Liste complète des métadonnées

Contributeur : Didier Rémy <>
Soumis le : jeudi 11 décembre 2014 - 09:03:22
Dernière modification le : jeudi 9 février 2017 - 15:25:26
Document(s) archivé(s) le : jeudi 12 mars 2015 - 10:15:13


Fichiers produits par l'(les) auteur(s)




Didier Rémy, Boris Yakobowski. A Church-Style Intermediate Language for MLF. Theoretical Computer Science, Elsevier, 2012, 435, pp.77--105. 〈http://dx.doi.org/10.1016/j.tcs.2012.02.026〉. 〈10.1016/j.tcs.2012.02.026〉. 〈hal-01093719〉



Consultations de
la notice


Téléchargements du document