Abstract
The framework Pure Type System (\(\mathcal{PTS}\)) offers a simple and general approach to designing and formalizing type systems. However, in the presence of dependent types, there often exist some acute problems that make it difficult for \(\mathcal{PTS}\) to accommodate many common realistic programming features such as general recursion, recursive types, effects (e.g., exceptions, references, input/output), etc. In this paper, we propose a new framework Applied Type System (\(\mathcal{ATS}\)) to allow for designing and formalizing type systems that can readily support common realistic programming features. The key salient feature of \(\mathcal{ATS}\) lies in a complete separation between statics, in which types are formed and reasoned about, and dynamics, in which programs are constructed and evaluated. With this separation, it is no longer possible for a program to occur in a type as is otherwise allowed in \(\mathcal{PTS}\). We present not only a formal development of \(\mathcal{ATS}\) but also mention some examples in support of using \(\mathcal{ATS}\) as a framework to form type systems for practical programming.
Partially supported by NSF grants no. CCR-0224244 and no. CCR-0229480
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, pp. 117–441. Clarendon Press, Oxford (1992)
Constable, R.L., Smith, S.F.: Partial objects in constructive type theory. In: Proceedings of Symposium on Logic in Computer Science, Ithaca, New York, June 1987, pp. 183–193 (1987)
Chen, C., Xi, H.: Meta-Programming through Typeful Code Representation. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, Uppsala, Sweden, August 2003, pp. 169–180 (2003)
Harper, R.: A simplified account of polymorphic references. Information Processing Letters 51, 201–206 (1994)
Honsell, F., Mason, I.A., Smith, S., Talcott, C.: A variable typed logic of effects. Information and Computation 119(1), 55–90 (1995)
Hayashi, S., Nakano, H.: PX: A Computational Logic. MIT Press, Cambridge (1988)
Jones, M.P.: Qualified Types: Theory and Practice, November 1994. Cambridge University Press, Cambridge (1994)
Mendler, N.P.: Recursive types and type constraints in second-order lambda calculus. In: Proceedings of Symposium on Logic in Computer Science, June 1987, pp. 30–36. The Computer Society of the IEEE, Los Alamitos (1987)
Paulin-Mohring, C.: Inductive Definitions in the System Coq: Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993)
Pfenning, F., Paulin-Mohring, C.: Inductively defined types in the Calculus of Constructions. In: Schmidt, D.A., Main, M.G., Melton, A.C., Mislove, M.W. (eds.) MFPS 1989. LNCS, vol. 442, pp. 209–228. Springer, Heidelberg (1990)
Shao, Z., Saha, B., Trifonov, V., Papaspyrou, N.: A Type System for Certified Binaries. In: Proceedings of 29th Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2002), Portland, OR, January 2002, pp. 217–232 (2002)
Xi, H., Chen, C., Chen, G.: Guarded Recursive Datatype Constructors (2002), Available at http://www.cs.bu.edu/~hwxi/GRecTypecon/
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, January 2003, pp. 224–235 (2003)
Xi, H.: Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, viii+181 pp. pp. viii+189. Available as (1998), http://www.cs.cmu.edu/~hwxi/DML/thesis.ps
Xi, H.: Applied Type System, Available at (July 2003), http://www.cs.bu.edu/~hwxi/ATS/ATS.ps
Xi, H., Pfenning, F.: Dependent Types in Practical Programming. In: Proceedings of 26th ACM SIGPLAN Symposium on Principles of Programming Languages, San Antonio, Texas, January 1999, pp. 214–227 (1999)
Zenger, C.: Indexed types. Theoretical Computer Science 187, 147–165 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Xi, H. (2004). Applied Type System. In: Berardi, S., Coppo, M., Damiani, F. (eds) Types for Proofs and Programs. TYPES 2003. Lecture Notes in Computer Science, vol 3085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24849-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-24849-1_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22164-7
Online ISBN: 978-3-540-24849-1
eBook Packages: Springer Book Archive