Paper Info
Title
A Church-Style Intermediate Language for MLF
Abstract
MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System F explicit first-class polymor- phism. We present xMLF, a Church-style version of MLF with full type information that can easily be maintained during reduction. All parame- ters of functions are explicitly typed and both type abstraction and type instantiation are explicit. However, type instantiation in xMLF is more general than type application in System F. We equip xMLF with a small- step reduction semantics that allows reduction in any context and show that this relation is confluent and type preserving. We also show that both subject reduction and progress hold for weak-reduction strategies, includ- ing call-by-value with the value-restriction. We exhibit a type preserving encoding of MLF into xMLF, which ensures type soundness for the most general version of MLF. We observe that xMLF is a calculus of retyping functions at the type level.
Year
DOI
Venue
2012
10.1007/978-3-642-12251-4_4
international symposium on functional and logic programming
Keywords
Field
DocType
type instantiation,full type information,type abstraction,type application,type inference,type soundness,type system,present xMLF,small-step reduction semantics,subject reduction,church-style intermediate language
Abstraction,Computer science,Subject reduction,Parametric polymorphism,Algorithm,Type inference,Theoretical computer science,Intermediate language,Semantics,Type class
Journal
Volume
ISSN
ISBN
435,
0302-9743
3-642-12250-7
Citations 
PageRank 
References 
6
0.57
9
Authors
2
Name
Order
Citations
PageRank
Didier Rémy168249.82
Boris Yakobowski219910.77