{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:33:21Z","timestamp":1754487201517},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540290513"},{"type":"electronic","value":"9783540317302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11559306_19","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T08:50:36Z","timestamp":1127811036000},"page":"310-320","source":"Crossref","is-referenced-by-count":14,"title":["ATS: A Language That Combines Programming with Theorem Proving"],"prefix":"10.1007","author":[{"given":"Sa","family":"Cui","sequence":"first","affiliation":[]},{"given":"Kevin","family":"Donnelly","sequence":"additional","affiliation":[]},{"given":"Hongwei","family":"Xi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"H.P. Barendregt","year":"1992","unstructured":"Barendregt, H.P.: Lambda Calculi with Types. In: Abramsky, S., Gabbay, D.M., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol.\u00a0II, pp. 117\u2013441. Clarendon Press, Oxford (1992)"},{"key":"19_CR2","series-title":"An EATCS Series","volume-title":"Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-24836-1_3","volume-title":"Practical Aspects of Declarative Languages","author":"C. Chen","year":"2004","unstructured":"Chen, C., Shi, R., Xi, H.: A Typeful Approach to Object-Oriented Programming with Multiple Inheritance. In: Jayaraman, B. (ed.) PADL 2004. LNCS, vol.\u00a03057, pp. 23\u201338. Springer, Heidelberg (2004)"},{"key":"19_CR4","unstructured":"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"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Chen, C., Xi, H.: Combining Programming with Theorem Proving (November 2004), http:\/\/www.cs.bu.edu\/~hwxi\/ATS\/PAPER\/CPwTP.ps","DOI":"10.1145\/1086365.1086375"},{"key":"19_CR6","volume-title":"Implementing Mathematics with the NuPrl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., et al: Implementing Mathematics with the NuPrl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"19_CR7","unstructured":"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\u2013193 (1987)"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/0097-3165(73)90004-6","volume":"14","author":"G. Dantzig","year":"1973","unstructured":"Dantzig, G., Eaves, B.: Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory (A)\u00a014, 288\u2013297 (1973)","journal-title":"Journal of Combinatorial Theory (A)"},{"key":"19_CR9","volume-title":"PX: A Computational Logic","author":"S. Hayashi","year":"1988","unstructured":"Hayashi, S., Nakano, H.: PX: A Computational Logic. The MIT Press, Cambridge (1988)"},{"issue":"1","key":"19_CR10","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1006\/inco.1995.1077","volume":"119","author":"F. Honsell","year":"1995","unstructured":"Honsell, F., Mason, I.A., Smith, S., Talcott, C.: A variable typed logic of effects. Information and Computation\u00a0119(1), 55\u201390 (1995)","journal-title":"Information and Computation"},{"key":"19_CR11","first-page":"30","volume-title":"Proceedings of Symposium on Logic in Computer Science","author":"N. Mendler","year":"1987","unstructured":"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\u201336. The Computer Society of the IEEE, Los Alamitos (1987)"},{"key":"19_CR12","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"R. Milner","year":"1997","unstructured":"Milner, R., Tofte, M., Harper, R.W., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)"},{"key":"19_CR13","first-page":"199","volume-title":"ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation","author":"F. Pfenning","year":"1998","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, Atlanta, Georgia, July 1988, vol.\u00a023(7), pp. 199\u2013208. ACM Press, New York (1998)"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-540-24849-1_25","volume-title":"Types for Proofs and Programs","author":"H. Xi","year":"2004","unstructured":"Xi, H.: Applied Type System (extended abstract). In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 394\u2013408. Springer, Heidelberg (2004)"},{"key":"19_CR15","unstructured":"Xi, H.: Applied Type System (2005), http:\/\/www.cs.bu.edu\/~hwxi\/ATS"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-30557-6_8","volume-title":"Practical Aspects of Declarative Languages","author":"D. Zhu","year":"2005","unstructured":"Zhu, D., Xi, H.: Safe Programming with Pointers through Stateful Views. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol.\u00a03350, pp. 83\u201397. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11559306_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:49:22Z","timestamp":1605624562000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11559306_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540290513","9783540317302"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11559306_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}