@InProceedings {Montagu-Remy@popl09:fzip,
AUTHOR = 
  {Beno{\^\i}t Montagu and Didier R{\'e}my},
TITLE =  
  {Modeling Abstract Types in Modules with Open Existential Types},
BOOKTITLE = 
  {Proceedings of the 36th {ACM} Symposium on Principles
  of Programming Languages (POPL'09)},
YEAR =         
  {2009},
ADDRESS =   
  {Savannah, Georgia, USA},
MONTH =     
  jan,
ALSO  =  {http://gallium.inria.fr/~remy/modules/},
PDF =    {http://gallium.inria.fr/~remy/modules/Montagu-Remy@popl09:fzip.pdf},
pages = {63--74},
ABSTRACT = 
  {We propose Fzip, a calculus of open existential types that is an
  extension of System F obtained by decomposing the introduction and
  elimination of  existential types into more atomic constructs. Open
  existential types model modular type abstraction as done in module
  systems. The static semantics of Fzip adapts standard techniques to deal
   with linearity of typing contexts,  its dynamic semantics is a
  small-step reduction semantics that  performs extrusion of type
  abstraction as needed during reduction, and the two are related by
  subject reduction and progress lemmas. Applying the Curry-Howard
  isomorphism,  Fzip can be also read back as a logic with the same
  expressive power as second-order logic but with more modular ways of
  assembling partial proofs. We also extend the core calculus to handle
  the double vision problem as well as type-level and term-level
  recursion. The resulting language turns out to be a new formalization of
  (a minor variant of) Dreyer's internal language for recursive and mixin
  modules.}
}