{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:15:35Z","timestamp":1725459335151},"publisher-location":"Berlin\/Heidelberg","reference-count":11,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540565175"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037094","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"1-12","source":"Crossref","is-referenced-by-count":19,"title":["On Mints' reduction for ccc-calculus"],"prefix":"10.1007","author":[{"given":"Yohji","family":"Akama","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"H.P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North Holland, second edition, 1984."},{"key":"1_CR2","first-page":"291","volume-title":"Proceedings ICALP '91","author":"P.-L. Curien","year":"1991","unstructured":"P.-L. Curien and R. Di Cosmo. A confluent reduction for the \u03bb-calculus with surjective pairing and terminal object. In Proceedings ICALP '91, Madrid, pages 291\u2013302. Springer-Verlag, 1991."},{"key":"1_CR3","unstructured":"D.\u010cubri\u0107. On free CCC. manuscript, March 12, 1992."},{"key":"1_CR4","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"1_CR5","unstructured":"M. Hgiya. Personal communication, Aug. 1991."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"M. agiya. From programming-by-example to proving-by-example. In T. Ito and A.R. Meyer, editors, Theoretical Aspects of Computer Software. Proceedings, pages 387\u2013419. Springer-Verlag, 1991. Lecture Notes in Computer Science, 526.","DOI":"10.1007\/3-540-54415-1_56"},{"key":"1_CR7","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G.P. Huet","year":"1975","unstructured":"G.P. Huet. A unification algorithm for typed lambda-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"1_CR8","unstructured":"C. Barry Jay. Long \u03b2\u03b7 normal forms and confluence(revised). LFCS, Department of Computer Science, University of Edinburgh, February 1992."},{"key":"1_CR9","unstructured":"J. Lambek and P.J. Scott. Introduction to higher order categorical logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, 1986."},{"key":"1_CR10","unstructured":"G.E. Mints. Theory of categories and theory of proofs. i. In Urgent Questions of Logic and the Methodology of Science, 1979. [in Russian], Kiev."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"D. Pawitz. Ideas and results in proof theory. In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 235\u2013307. North-Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70849-8"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037094.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:21:58Z","timestamp":1607552518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037094"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0037094","relation":{},"subject":[]}}