{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:56:55Z","timestamp":1725562615515},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221647"},{"type":"electronic","value":"9783540248491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_25","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T20:34:24Z","timestamp":1281299664000},"page":"394-408","source":"Crossref","is-referenced-by-count":27,"title":["Applied Type System"],"prefix":"10.1007","author":[{"given":"Hongwei","family":"Xi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"25_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.S.E. (eds.) Handbook of Logic in Computer Science, pp. 117\u2013441. Clarendon Press, Oxford (1992)"},{"key":"25_CR2","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":"25_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013180 (2003)","DOI":"10.1145\/944705.944730"},{"key":"25_CR4","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0020-0190(94)90120-1","volume":"51","author":"R. Harper","year":"1994","unstructured":"Harper, R.: A simplified account of polymorphic references. Information Processing Letters\u00a051, 201\u2013206 (1994)","journal-title":"Information Processing Letters"},{"issue":"1","key":"25_CR5","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":"25_CR6","volume-title":"PX: A Computational Logic","author":"S. Hayashi","year":"1988","unstructured":"Hayashi, S., Nakano, H.: PX: A Computational Logic. MIT Press, Cambridge (1988)"},{"key":"25_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663086","volume-title":"Qualified Types: Theory and Practice","author":"M.P. Jones","year":"1994","unstructured":"Jones, M.P.: Qualified Types: Theory and Practice, November 1994. Cambridge University Press, Cambridge (1994)"},{"key":"25_CR8","first-page":"30","volume-title":"Proceedings of Symposium on Logic in Computer Science","author":"N.P. Mendler","year":"1987","unstructured":"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\u201336. The Computer Society of the IEEE, Los Alamitos (1987)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive Definitions in the System Coq: Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 328\u2013345. Springer, Heidelberg (1993)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/BFb0040259","volume-title":"Mathematical Foundations of Programming Semantics","author":"F. Pfenning","year":"1990","unstructured":"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.\u00a0442, pp. 209\u2013228. Springer, Heidelberg (1990)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"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\u2013232 (2002)","DOI":"10.1145\/503272.503293"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Xi, H., Chen, C., Chen, G.: Guarded Recursive Datatype Constructors (2002), Available at http:\/\/www.cs.bu.edu\/~hwxi\/GRecTypecon\/","DOI":"10.1145\/604131.604150"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013235 (2003)","DOI":"10.1145\/604131.604150"},{"key":"25_CR14","unstructured":"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"},{"key":"25_CR15","unstructured":"Xi, H.: Applied Type System, Available at (July 2003), http:\/\/www.cs.bu.edu\/~hwxi\/ATS\/ATS.ps"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"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\u2013227 (1999)","DOI":"10.1145\/292540.292560"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0304-3975(97)00062-5","volume":"187","author":"C. Zenger","year":"1997","unstructured":"Zenger, C.: Indexed types. Theoretical Computer Science\u00a0187, 147\u2013165 (1997)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:57:41Z","timestamp":1605761861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}