{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:07:41Z","timestamp":1725574061481},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540240877"},{"type":"electronic","value":"9783540305026"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30502-6_32","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T22:22:20Z","timestamp":1294438940000},"page":"437-451","source":"Crossref","is-referenced-by-count":0,"title":["A Simple Theory of Expressions, Judgments and Derivations"],"prefix":"10.1007","author":[{"given":"Masahiko","family":"Sato","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","series-title":"Texts in Theoretical Computer Science","volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. In: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"32_CR2","first-page":"98","volume-title":"Symbolic Computation and Automated Reasoning, Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning","author":"B. Buchberger","year":"2000","unstructured":"Buchberger, B., Dupre, C., Jebelean, T., Kriftner, F., Nakagawa, K., Vasaru, D., Windsteiger, W.: The Theorema Project: A Progress Report. In: Kerber, M., Kohlhase, M. (eds.) Symbolic Computation and Automated Reasoning, Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, St. Andrews, Scotland, August 6-7, pp. 98\u2013113. A.K. Peters, Natick (2000)"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabell\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabell\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"32_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/3-540-45654-6_40","volume-title":"Computer Aided Systems Theory \u2013 EUROCAST 2001","author":"M. Sato","year":"2001","unstructured":"Sato, M., Kameyama, Y., Takeuti, I.: CAL: A computer assisted learning system for computation and logic. In: Moreno-Diaz, R., Buchberger, B., Freire, J.-L. (eds.) Computer Aided Systems Theory \u2013 EUROCAST 2001. LNCS, vol.\u00a02718, pp. 509\u2013524. Springer, Heidelberg (2001)"},{"key":"32_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45884-0_5","volume-title":"Progress in Discovery Science","author":"M. Sato","year":"2002","unstructured":"Sato, M.: Theory of Judgments and Derivations, in Arikawa. In: Arikawa, S., Shinohara, A. (eds.) Progress in Discovery Science. LNCS (LNAI), vol.\u00a02281, pp. 78\u2013122. Springer, Heidelberg (2002)"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Sato, M., Sakurai, T., Kameyama, Y.: A Simply Typed Context Calculus with First-Class Environments. Journal of Functional and Logic Programming\u00a02002(4) (March 2002)","DOI":"10.1007\/3-540-44716-4_23"},{"key":"32_CR7","unstructured":"Vestergaard, R.: The primitive proof theory of the \u03bb-calculus. PhD thesis, School of Maths and Computer Sciences, Heriot-Watt University (2003)"}],"container-title":["Lecture Notes in Computer Science","Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30502-6_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:57:59Z","timestamp":1605761879000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30502-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540240877","9783540305026"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30502-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}