Abstract
ATS is a language with a highly expressive type system that supports a restricted form of dependent types in which programs are not allowed to appear in type expressions. The language is separated into two components: a proof language in which (inductive) proofs can be encoded as (total recursive) functions that are erased before execution, and a programming language for constructing programs to be evaluated. This separation enables a paradigm that combines programming with theorem proving. In this paper, we illustrate by example how this programming paradigm is supported in ATS.
This is a preview of subscription content, log in via an institution to check access.
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. (eds.) Handbook of Logic in Computer Science, vol. II, pp. 117–441. Clarendon Press, Oxford (1992)
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)
Chen, C., Shi, R., Xi, H.: A Typeful Approach to Object-Oriented Programming with Multiple Inheritance. In: Jayaraman, B. (ed.) PADL 2004. LNCS, vol. 3057, pp. 23–38. Springer, Heidelberg (2004)
Chen, C., Xi, H.: ATS/LF: a type system for constructing proofs as total functional programs (November 2004), http://www.cs.bu.edu/~hwxi/ATS/PAPER/ATSLF.ps
Chen, C., Xi, H.: Combining Programming with Theorem Proving (November 2004), http://www.cs.bu.edu/~hwxi/ATS/PAPER/CPwTP.ps
Constable, R.L., et al: Implementing Mathematics with the NuPrl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)
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)
Dantzig, G., Eaves, B.: Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory (A) 14, 288–297 (1973)
Hayashi, S., Nakano, H.: PX: A Computational Logic. The MIT Press, Cambridge (1988)
Honsell, F., Mason, I.A., Smith, S., Talcott, C.: A variable typed logic of effects. Information and Computation 119(1), 55–90 (1995)
Mendler, N.: Recursive types and type constraints in second-order lambda calculus. In: Proceedings of Symposium on Logic in Computer Science, Ithaca, New York, June 1987, pp. 30–36. The Computer Society of the IEEE, Los Alamitos (1987)
Milner, R., Tofte, M., Harper, R.W., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)
Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, Atlanta, Georgia, July 1988, vol. 23(7), pp. 199–208. ACM Press, New York (1998)
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.: Applied Type System (2005), http://www.cs.bu.edu/~hwxi/ATS
Zhu, D., Xi, H.: Safe Programming with Pointers through Stateful Views. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol. 3350, pp. 83–97. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cui, S., Donnelly, K., Xi, H. (2005). ATS: A Language That Combines Programming with Theorem Proving. In: Gramlich, B. (eds) Frontiers of Combining Systems. FroCoS 2005. Lecture Notes in Computer Science(), vol 3717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11559306_19
Download citation
DOI: https://doi.org/10.1007/11559306_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29051-3
Online ISBN: 978-3-540-31730-2
eBook Packages: Computer ScienceComputer Science (R0)