{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:27:54Z","timestamp":1725488874678},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439165"},{"type":"electronic","value":"9783540456100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45610-4_14","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T06:47:11Z","timestamp":1186901231000},"page":"192-206","source":"Crossref","is-referenced-by-count":1,"title":["Tradeoffs in the Intensional Representation of Lambda Terms"],"prefix":"10.1007","author":[{"given":"Chuck","family":"Liang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gopalan","family":"Nadathur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"issue":"4","key":"14_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 1(4):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1016\/0022-0000(81)90073-8","volume":"23","author":"L. Aiello","year":"1981","unstructured":"L. Aiello and G. Prini. An efficient interpreter for the lambda-calculus. The Journal of Computer and System Sciences, 23:383\u2013425, 1981.","journal-title":"The Journal of Computer and System Sciences"},{"issue":"5","key":"14_CR3","doi-asserted-by":"crossref","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Z. Benaissa","year":"1996","unstructured":"Z. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. \u03bbGU, a calculus of explicit substitutions which preserves strong normalization. Journal of Functional Programming, 6(5):699\u2013722, 1996.","journal-title":"Journal of Functional Programming"},{"issue":"5","key":"14_CR4","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. Bruijn de","year":"1972","unstructured":"N. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indag. Math., 34(5):381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"14_CR5","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"14_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44716-4_8","volume-title":"Fifth International Symposium on Functional and Logic Programming","author":"G. Delzanno","year":"2001","unstructured":"G. Delzanno. Specifying and debugging security protocols via hereditary Harrop formulas and \u03bbProlog-a case-study. In Fifth International Symposium on Functional and Logic Programming. Springer Verlag LNCS vol. 2024, 2001."},{"key":"14_CR7","volume-title":"Rapport Techniques 154","author":"G. Dowek","year":"1993","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user\u2019s guide. Rapport Techniques 154, INRIA, Rocquencourt, France, 1993."},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G. Dowek","year":"2000","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. Information and Computation, 157:183\u2013235, 2000.","journal-title":"Information and Computation"},{"issue":"1","key":"14_CR9","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"4","key":"14_CR10","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1017\/S0956796897002785","volume":"7","author":"F. Kamareddine","year":"1997","unstructured":"F. Kamareddine and A. R\u00edos. Extending the \u03bb-calculus with explicit substitution which preserves strong normalization into a confluent calculus on open terms. Journal of Functional Programming, 7(4):395\u2013420, 1997.","journal-title":"Journal of Functional Programming"},{"key":"14_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-45587-6_5","volume-title":"4th International Symposium on Practical Aspects of Declarative Languages","author":"C. Liang","year":"2002","unstructured":"C. Liang. Compiler construction in higher order logic programming. In 4th International Symposium on Practical Aspects of Declarative Languages, pages 47\u201363. Springer Verlag LNCS No. 2257, 2002."},{"issue":"4","key":"14_CR12","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"D. Miller. A logic programming language with \u03bb-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497\u2013536, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"D. Miller. Unification under a mixed prefix. Journal of Symbolic Computation, pages 321\u2013358, 1992.","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"14_CR14","unstructured":"M. Mottl. Automating functional program transformation. MSc Thesis. Division of Informatics, University of Edinburgh, September 2000."},{"key":"14_CR15","unstructured":"G. Nadathur. A fine-grained notation for lambda terms and its use in intensional operations. Journal of Functional and Logic Programming, 1999(2), March 1999."},{"key":"14_CR16","unstructured":"G. Nadathur and D. Miller. An overview of \u03bbProlog. In K. A. Bowen and R. A. Kowalski, editors, Fifth International Logic Programming Conference, pages 810\u2013827. MIT Press, August 1988."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"G. Nadathur and D. J. Mitchell. System description: Teyjus\u2014a compiler and abstract machine based implementation of \u03bbProlog. In Automated Deduction-CADE-16, pages 287\u2013291. Springer-Verlag LNAI no. 1632, 1999.","DOI":"10.1007\/3-540-48660-7_25"},{"issue":"1\u20132","key":"14_CR18","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(97)00184-9","volume":"198","author":"G. Nadathur","year":"1998","unstructured":"G. Nadathur and D. S. Wilson. A notation for lambda terms: A generalization of environments. Theoretical Computer Science, 198(1\u20132):49\u201398, 1998.","journal-title":"Theoretical Computer Science"},{"key":"14_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq: Rules and properties. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 328\u2013345. Springer-Verlag LNCS 664, 1993."},{"key":"14_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer Verlag, 1994."},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Sch\u00fcrmann. System description: Twelf\u2014a meta-logical framework for deductive systems. In Proceedings of the 16th International Conference on Automated Deduction, pages 202\u2013206. Springer-Verlag LNAI 1632, 1999.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Z. Shao. Implementing typed intermediate language. In Proc. 1998 ACM SIG-PLAN International Conference on Functional Programming (ICFP\u201998), pages 313\u2013323. ACM Press, September 1998.","DOI":"10.1145\/289423.289460"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In 1996 SIGPLAN Conference on Programming Language Design and Implementation, pages 181\u2013192. ACM Press, 1996.","DOI":"10.1145\/231379.231414"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45610-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:54:41Z","timestamp":1556754881000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45610-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439165","9783540456100"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45610-4_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}