{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:00:32Z","timestamp":1725487232145},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540727323"},{"type":"electronic","value":"9783540727347"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-72734-7_2","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T09:40:50Z","timestamp":1183023650000},"page":"12-25","source":"Crossref","is-referenced-by-count":10,"title":["The Intensional Lambda Calculus"],"prefix":"10.1007","author":[{"given":"Sergei","family":"Artemov","sequence":"first","affiliation":[]},{"given":"Eduardo","family":"Bonelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-45504-3_2","volume-title":"Proof Theory in Computer Science","author":"J. Alt","year":"2001","unstructured":"Alt, J., Artemov, S.N.: Reflective \u03bb-calculus. In: Kahle, R., Schroeder-Heister, P., St\u00e4rk, R.F. (eds.) PTCS 2001. LNCS, vol.\u00a02183, p. 22. Springer, Heidelberg (2001)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Artemov, S., Bonelli, E.: The intensional lambda calculus. Technical report (December 2006), http:\/\/www.lifia.info.unlp.edu.ar\/~eduardo\/lamIFull.pdf","DOI":"10.1007\/978-3-540-72734-7_2"},{"key":"2_CR3","unstructured":"Artemov, S.: Operational modal logic. Technical Report MSI 95-29, Cornell University (1995)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Artemov, S.: Proof realization of intuitionistic and modal logics. Technical Report MSI 96-06, Cornell University (1996)","DOI":"10.21236\/ADA344305"},{"key":"2_CR5","unstructured":"Artemov, S.: Unified semantics of modality and \u03bb-terms via proof polynomials. In: Algebras, Diagrams and Decisions in Language, Logic and Computation, pp. 89\u2013118 (2001)"},{"key":"2_CR6","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, vol.\u00a02, Oxford University Press, Oxford (1992)"},{"key":"2_CR7","unstructured":"Brezhnev, V.: On the logic of proofs. In: Striegnitz, K. (ed.) Proceedings of the Sixth ESSLLI Student Session, pp. 35\u201345 (2001)"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"472","DOI":"10.2307\/1989762","volume":"39","author":"A. Church","year":"1936","unstructured":"Church, A., Rosser, J.B.: Some properties of conversion. Transactions of the American Mathematical Society\u00a039, 472\u2013482 (1936)","journal-title":"Transactions of the American Mathematical Society"},{"key":"2_CR9","first-page":"258","volume-title":"Proceedings of the 23rd Annual Symposium on Principles of Programming Languages","author":"R. Davies","year":"1996","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. In: Steele Jr., G. (ed.) Proceedings of the 23rd Annual Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, January 1996, pp. 258\u2013270. ACM Press, New York (1996)"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"R. Davies","year":"2001","unstructured":"Davies, R., Pfenning, F.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science\u00a011, 511\u2013540 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"3","key":"2_CR11","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/382780.382785","volume":"48","author":"R. Davies","year":"2001","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of the ACM\u00a048(3), 555\u2013604 (2001)","journal-title":"Journal of the ACM"},{"key":"2_CR12","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1989)"},{"key":"2_CR13","first-page":"394","volume-title":"Computational Logic; Essays in honor of Alan Robinson","author":"G. Huet","year":"1991","unstructured":"Huet, G., L\u00e9vy, J.-J.: Computations in orthogonal rewriting systems. In: Lassez, J.L., Plotkin, G.D. (eds.) Computational Logic; Essays in honor of Alan Robinson, pp. 394\u2013443. MIT Press, Cambridge (1991)"},{"key":"2_CR14","unstructured":"Klop, J.W.: Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam, Mathematical Centre Tracts no.127 (1980)"},{"key":"2_CR15","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1006\/inco.2000.2888","volume":"164","author":"Z. Khasidashvili","year":"2001","unstructured":"Khasidashvili, Z., Ogawa, M., van Oostrom, V.: Perpetuality and uniform normalization in orthogonal rewrite systems. Information and Computation\u00a0164, 118\u2013151 (2001)","journal-title":"Information and Computation"},{"key":"2_CR16","unstructured":"L\u00e9vy, J.-J.: R\u00e9ductions correctes et optimales dans le lambda-calcul. PhD thesis, Universit\u00e9 Paris VII (1978)"},{"key":"2_CR17","unstructured":"Martin-L\u00f6f, P.: On the meaning of the logical constants and the justifications of the logical laws. Lectures given at the meeting Teoria della Dimostrazione e Filosofia della Logica, in Siena, 6-9 April 1983, by the Scuola di Specializzazione in Logica Matematica of the Universit\u00e0 degli Studi di Siena (1983)"},{"key":"2_CR18","volume-title":"Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science","author":"T. Nipkow","year":"1991","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, July 1991, IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"2_CR19","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Term Rewriting Systems","author":"TERESE","year":"2003","unstructured":"TERESE: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press, Cambridge (March 2003)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Wickline, P., Lee, P., Pfenning, F., Davies, R.: Modal types as staging specifications for run-time code generation. ACM Computing Surveys\u00a030(3es) (1998)","DOI":"10.1145\/289121.289129"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72734-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,23]],"date-time":"2020-04-23T19:19:13Z","timestamp":1587669553000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72734-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540727323","9783540727347"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72734-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}