{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:17:39Z","timestamp":1725484659473},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425540"},{"type":"electronic","value":"9783540448020"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_30","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:15:38Z","timestamp":1180656938000},"page":"429-442","source":"Crossref","is-referenced-by-count":0,"title":["Life without the Terminal Type"],"prefix":"10.1007","author":[{"given":"Lutz","family":"Schr\u00f6der","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"30_CR1","volume-title":"Abstract and concrete categories","author":"J. Ad\u00e1mek","year":"1990","unstructured":"J. Ad\u00e1mek, H. Herrlich, and G. E. Strecker, Abstract and concrete categories, Wiley, New York, 1990."},{"key":"30_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0022243","volume-title":"Computer Science Logic","author":"D. Aspinall","year":"1995","unstructured":"D. Aspinall, Subtyping with singleton types, Computer Science Logic, LNCS, vol. 933, Springer, 1995, pp. 1\u201315."},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"F. Borceux, Handbook of categorical algebra 1, Cambridge, 1994.","DOI":"10.1017\/CBO9780511525865"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"R. L. Crole, Categories for types, Cambridge, 1994.","DOI":"10.1017\/CBO9781139172707"},{"key":"30_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0317-9","volume-title":"Categorical combinators, sequential algorithms, and functional programming","author":"P.-L. Curien","year":"1993","unstructured":"P.-L. Curien, Categorical combinators, sequential algorithms, and functional programming. 2nd ed., Birkh\u00e4user, Boston, 1993.","edition":"2nd ed."},{"key":"30_CR6","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1017\/S0956796800001696","volume":"6","author":"P.-L. Curien","year":"1996","unstructured":"P.-L. Curien and R. Di Cosmo, A confluent reduction for the \u03bb-calculus with surjective pairing and terminal object, J. Funct. Programming 6 (1996), 299\u2013327.","journal-title":"J. Funct. Programming"},{"key":"30_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-61464-8_53","volume-title":"Rewriting Techniques and Applications","author":"R. Cosmo Di","year":"1996","unstructured":"R. Di Cosmo, On the power of simple diagrams, Rewriting Techniques and Applications, LNCS, vol. 1103, Springer, 1996, pp. 200\u2013214."},{"key":"30_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/3-540-61377-3_40","volume-title":"Computer Science Logic","author":"R. Cosmo Di","year":"1996","unstructured":"R. Di Cosmo and D. Kesner, Rewriting with polymorphic extensional \u03bb-calculus, Computer Science Logic, LNCS, vol. 1092, Springer, 1996, pp. 215\u2013232."},{"key":"30_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/3-540-62688-3_35","volume-title":"Typed Lambda Calculus and Applications","author":"N. Ghani","year":"1997","unstructured":"N. Ghani, Eta-expansions in dependent type theory \u2014 the calculus of constructions, Typed Lambda Calculus and Applications, LNCS, vol. 1210, Springer, 1997, pp. 164\u2013180."},{"key":"30_CR10","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(89)90105-9","volume":"65","author":"T. Hardin","year":"1989","unstructured":"T. Hardin, Confluence results for the pure strong categorical logic CCL; lambda-calculi as subsystems of CCL, Theoret. Comput. Sci. 65 (1989), 291\u2013342.","journal-title":"Theoret. Comput. Sci."},{"key":"30_CR11","volume-title":"Categorical logic and type theory","author":"B. Jacobs","year":"1999","unstructured":"B. Jacobs, Categorical logic and type theory, Elsevier, Amsterdam, 1999."},{"key":"30_CR12","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"C. B. Jay","year":"1995","unstructured":"C. B. Jay and N. Ghani, The virtues of eta-expansion, J. Funct. Programming 5 (1995), 135\u2013154.","journal-title":"J. Funct. Programming"},{"key":"30_CR13","volume-title":"Models of the lambda calculus","author":"C. P. J. Koymans","year":"1984","unstructured":"C. P. J. Koymans, Models of the lambda calculus, CWI, Amsterdam, 1984."},{"key":"30_CR14","unstructured":"J. Lambek and P. J. Scott, Introduction to higher order categorical logic, Cambridge, 1986."},{"key":"30_CR15","unstructured":"S. Mac Lane, Categories for the working mathematician, Springer, 1997."},{"key":"30_CR16","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0890-5401(87)90018-6","volume":"73","author":"A. Obtulowicz","year":"1987","unstructured":"Adam Obtulowicz, Algebra of constructions I. The word problem for partial algebras, Inform. and Comput. 73 (1987), 129\u2013173.","journal-title":"Inform. and Comput."},{"key":"30_CR17","series-title":"Lect Notes Comput Sci","first-page":"58","volume-title":"Category Theory and Computer Programming","author":"A. Poign\u00e9","year":"1985","unstructured":"Axel Poign\u00e9, Cartesian closure-higher types in categories, Category Theory and Computer Programming, LNCS, vol. 240, Springer, 1985, pp. 58\u201375."},{"key":"30_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/BF00370825","volume":"48","author":"P. H. Rodenberg","year":"1989","unstructured":"P. H. Rodenberg and F. J. van der Linden, Manufacturing a cartesian closed category with exactly two objects out of a C-monoid, Stud. Log. 48 (1989), 279\u2013283.","journal-title":"Stud. Log."},{"key":"30_CR19","unstructured":"D. S. Scott, Relating theories of the \u03bb-calculus, To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalisms, Academic Press, 1980, pp. 403\u2013450."},{"key":"30_CR20","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"R. A. G. Seely","year":"1984","unstructured":"R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Cambridge Philos. Soc. 95 (1984), 33\u201348.","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"key":"30_CR21","doi-asserted-by":"publisher","first-page":"969","DOI":"10.2307\/2273831","volume":"52","author":"R. A. G. Seely","year":"1987","unstructured":"R. A. G. Seely, Categorical semantics for higher order polymorphic lambda calclus, J. Symbolic Logic 52 (1987), 969\u2013989.","journal-title":"J. Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:21:16Z","timestamp":1556450476000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}