Abstract
A common approach to hiding implementation details is through the use of abstract types. In this paper, we present a simple theoretical account of abstract types that make use of a recently developed notion of conditional type equality. This is in contrast to most of the existing theoretical accounts of abstract types, which rely on existential types (or similar variants). In addition, we show that this new approach to abstract types opens a promising avenue to the design and implementation of module systems that can effectively support large-scale programming.
Partially supported by NSF grants no. CCR-0229480 and no. CCF-0702665.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Cardelli, L., Donahue, J., Jordan, M., Kalso, B., Nelson, G.: The Modula-3 Type System. In: Proceedings of 16th Annual ACM Symposium on Principles of Programming Languages (POPL 1989), Austin, TX, January 1989, pp. 202–212 (1989)
Crary, K., Harper, R., Puri, S.: What is a recursive module? In: SIGPLAN Conference on Programming Language Design and Implementation (PLDI 1999), June 1999, pp. 56–63 (1999)
Cardelli, L., Leroy, X.: Abstract Types and the Dot Notation. Technical Report 56, DEC SRC (1990)
Dreyer, D., Crary, K., Harper, R.: A Type System for Higher-Order Modules. In: Proceedings of 30th Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2003), New Orleans, LA, January 2003, pp. 236–249 (2003)
Guttag, J.V., Horning, J.J., Wing, J.M.: The Larch Family of Specification Languages. IEEE Software 2(5), 24–36 (1985)
Harper, R.W., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: Proceedings of 21st Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 1994), Portland, Oregon, pp. 123–137 (1994)
Leroy, X.: Manifest Types, Modules, and Separate Compilation. In: Proceeding of 21st Annual ACM Conference on Principles of Programming lanugages (POPL 1994), Porland, OR (January 1994)
Leroy, X.: Aplicative functors and fully transparent higher-order modules. In: Proceedings of 22nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 1995), San Francisco, CA, January 1995, pp. 142–153 (1995)
Lillibridge, M.: Translucent Sums: A Foundation for Higher-Order Module Systems. Ph. D. dissertation, Carnegie Mellon University (May 1997)
Liskov, B.: Abstraction and Specification in Program Development. MIT Press, Cambridge (1986)
MacQueen, D.B.: Using Dependent Types to Express Modular Structure. In: Proceeding of 13th Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, FL, pp. 277–286 (1986)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. In: Proceedings of 12th Annual ACM Symposium on Principles of Programming Languages (POPL 1985), New Orleans, Louisiana, pp. 37–51 (1985)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Transactions on Programming Languages and Systems 10(3), 470–502 (1988)
Milner, R., Tofte, M., Harper, R.W., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)
Russo, C.V.: First-Class Structures for Standard ML. Nordic Journal of Computing 7(4), 348–374 (2000)
Russo, C.V.: Recursive Structures for Standard ML. In: Proceedings of International Conference on Functional Programming, September 2001, pp. 50–61 (2001)
Sheldon, M.A., Gifford, D.K.: Static Dependent Types for First-Class Modules. In: Proceedings of ACM Conference on Lisp and Functional Programming, pp. 20–29 (1990)
Shields, M., Jones, S.P.: First-class modules for haskell. In: Proceedings of 9th International Workshop on Foundations of ObjectOriented Languages (FOOL 9), Portland, OR (January 2002)
Wirth, N.: Programming with Modula-2. Texts and Monographs in Computer Science. Springer, Heidelberg (1982)
Xi, H., Chen, C., Chen, G.: Guarded Recursive Datatype Constructors. In: Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages, New Orleans, LA, pp. 224–235. ACM press, New York (2003)
Xi, H.: The ATS Programming Language, http://www.ats-lang.org/
Xi, H.: Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University (1998), viii+181 pp. pp. viii+189, http://www.cs.cmu.edu/~hwxi/DML/thesis.ps
Xi, H.: Applied Type System (extended abstract). In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 394–408. Springer, Heidelberg (2004)
Xi, H., Pfenning, F.: Dependent Types in Practical Programming. In: Proceedings of 26th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 214–227. ACM Press, San Antonio (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xi, H. (2009). A Simple and General Theoretical Account for Abstract Types. In: Oliveira, M.V.M., Woodcock, J. (eds) Formal Methods: Foundations and Applications. SBMF 2009. Lecture Notes in Computer Science, vol 5902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10452-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-10452-7_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10451-0
Online ISBN: 978-3-642-10452-7
eBook Packages: Computer ScienceComputer Science (R0)