{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:59:19Z","timestamp":1725487159544},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540429593"},{"type":"electronic","value":"9783540456544"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45654-6_40","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:21:19Z","timestamp":1184588479000},"page":"509-524","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["CAL: A Computer Assisted Learning System for Computation and Logic"],"prefix":"10.1007","author":[{"given":"Masahiko","family":"Sato","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yukiyoshi","family":"Kameyama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takeuti","family":"Izumi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,2,8]]},"reference":[{"key":"40_CR1","unstructured":"Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, North-Holland, 1981."},{"key":"40_CR2","unstructured":"Barwise, J. and J. Etchemendy, Tarski\u2019s World, CSLI Lecture Notes, No. 25, CSLI Publications, Cambridge University Press, 1994."},{"key":"40_CR3","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"D. G. Bruijn de","year":"1972","unstructured":"de Bruijn, D. G., Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem, Indag. Math. 34, pp. 381\u2013392, 1972.","journal-title":"Indag. Math"},{"issue":"1","key":"40_CR4","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. F. Harper","year":"1993","unstructured":"Harper, R., F. Honsell, and G. Plotkin, A Framework for Defining Logics, Journal of the Association for Computing Machinery, Vol. 40, No. 1, pp. 143\u2013184, 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"40_CR5","doi-asserted-by":"crossref","unstructured":"Huet, G., and G. Plotkin eds., Logical Frameworks, Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807"},{"key":"40_CR6","unstructured":"Nordstr\u00f6m, B., K. Petersson, and J. M. Smith, Programming in Martin-L\u00f6f\u2019 s Type Theory, Oxford University Press, 200 pages, 1990."},{"key":"40_CR7","unstructured":"Sato, M., and M. Hagiya, Hyperlisp, in de Bakker, van Vliet eds., Algorithmic Languages, North-Holland, pp. 251\u2013269, 1981."},{"key":"40_CR8","doi-asserted-by":"publisher","first-page":"455","DOI":"10.2977\/prims\/1195179055","volume":"21","author":"M. Sato","year":"1985","unstructured":"Sato, M., Theory of Symbolic Expressions, II, Publ. of Res. Inst. for Math. Sci., Kyoto Univ., 21, pp. 455\u2013540, 1985.","journal-title":"Publ. of Res. Inst. for Math. Sci."},{"key":"40_CR9","doi-asserted-by":"crossref","unstructured":"Sato, M., An Abstraction Mechanism for Symbolic Expressions, in V. Lifschitz ed., Artificial Intelligence and Mathematical Theory of Computation (Papers in Honor of John McCarthy), Academic Press, pp. 381\u2013391, 1991.","DOI":"10.1016\/B978-0-12-450010-5.50027-X"},{"key":"40_CR10","first-page":"79","volume":"45","author":"M. Sato","year":"2001","unstructured":"Sato, M., T. Sakurai and R. Burstall, Explicit Environments, Fundamenta Informaticae 45, pp. 79\u2013115, 2001.","journal-title":"Fundamenta Informaticae"},{"key":"40_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-44716-4_23","volume-title":"Proc. Fifth International Symposium on Functional and Logic Programming (FLOPS)","author":"M. Sato","year":"2001","unstructured":"Sato, M., T. Sakurai and Y. Kameyama, A Simply Typed Context Calculus with First-Class Environments, Proc. Fifth International Symposium on Functional and Logic Programming (FLOPS), Lecture Notes in Computer Science 2024, pp. 359\u2013374, 2001."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Systems Theory \u2014 EUROCAST 2001"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45654-6_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T19:43:53Z","timestamp":1558467833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45654-6_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540429593","9783540456544"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-45654-6_40","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"8 February 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}