Modeling abstract types in modules with open existential types. (English) Zbl 1315.68103
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’09, Savannah, GA, USA, January 18–24, 2009. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-379-2). 354-365 (2009).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 03B70 | Logic in computer science |
| 68N18 | Functional programming and lambda calculus |
Keywords:
abstract types; existential types; generativity; lambda-calculus; linear type systems; modularity; modules; type systemsReferences:
| [1] | Luca Cardelli and Xavier Leroy. Abstract types and the dot notation. In M. Broy and C. B. Jones, editors, Proceedings IFIP TC2 working conference on programming concepts and methods, pages 479-504. North-Holland, 1990. |
| [2] | Derek Dreyer. Recursive type generativity. Journal of Functional Programming, pages 433-471, 2007. 10.1017/S0956796807006429 · Zbl 1125.68028 |
| [3] | Derek Dreyer. A type system for recursive modules. In Proceedings of ACM SIGPLAN International Conference on Functional Programming, pages 289-302, 2007. 10.1145/1291151.1291196 · Zbl 1291.68116 |
| [4] | Derek Dreyer, Karl Crary, and Robert Harper. A type system for higher-order modules. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, pages 236-249, 2003. 10.1145/604131.604151 · Zbl 1321.68167 |
| [5] | Matthew Flatt and Matthias Felleisen. Units: Cool modules for hot languages. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 236-248, 1998. 10.1145/277650.277730 |
| [6] | Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, pages 123-137, New York, NY, USA, 1994. ACM. 10.1145/174675.176927 |
| [7] | Robert Harper, John C. Mitchell, and Eugenio Moggi. Higher-order modules and the phase distinction. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, pages 341-354, San Francisco, CA, January 1990. 10.1145/96709.96744 |
| [8] | Robert Harper and Benjamin C. Pierce. Design considerations for ML-style module systems. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 8, pages 293-345. The MIT Press, 2005. · Zbl 1080.68009 |
| [9] | Daniel K. Lee, Karl Crary, and Robert Harper. Towards a mechanized metatheory of Standard ML. SIGPLAN Not., 42(1):173-184, 2007. 10.1145/1190215.1190245 |
| [10] | A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6(5):667-698, 1996. · Zbl 0872.68015 |
| [11] | Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Remy, and Jerome Vouillon. The Objective Caml system release 3.10. INRIA, May 2007. |
| [12] | David MacQueen. Modules for Standard ML. In ACM Symposium on LISP and functional programming, pages 198-207, New York, NY, USA, 1984. ACM. 10.1145/800055.802036 |
| [13] | Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). The MIT Press, May 1997. |
| [14] | John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. ACM Trans. Program. Lang. Syst., 10(3):470-502, 1988. 10.1145/44501.45065 |
| [15] | Benoit Montagu and Didier Remy. Towards a simpler account of modules and generativity: Abstract types have Open existential types. Available at http://gallium.inria.fr/remy/modules/, March 2008. |
| [16] | Martin Odersky, Vincent Cremet, Christine Rockl, and Matthias Zenger. A nominal theory of objects with dependent types. In Proceedings of European Conference on Object-Oriented Programming, pages 201-224, 2003. |
| [17] | Gilles Peskine. Abstract types in collaborative programs. PhD thesis, Universite Paris VII – Denis Diderot, June 2008. |
| [18] | John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing 83, pages 513-523. Elsevier Science, 1983. |
| [19] | Sergei Romanenko, Claudio Russo, and Peter Sestoft. Moscow ML Owner’s Manual, June 2000. |
| [20] | Andreas Rossberg. Generativity and dynamic opacity for abstract types. In Proceedings of ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 241-252, Uppsala, Sweden, September 2003. 10.1145/888251.888274 |
| [21] | Claudio V. Russo. Types for modules. Electronic Notes in Theoretical Computer Science, 60, January 2003. |
| [22] | Christopher A. Stone and Robert Harper. Deciding type equivalence in a language with singleton kinds. In Proceedings of ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 214-227, Boston, January 2000. 10.1145/325694.325724 · Zbl 1323.68163 |
| [23] | Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, 1994. 10.1006/inco.1994.1093 · Zbl 0938.68559 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
