{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:20Z","timestamp":1761611300386},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540630456"},{"type":"electronic","value":"9783540690658"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63045-7_2","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:00:19Z","timestamp":1330297219000},"page":"9-20","source":"Crossref","is-referenced-by-count":8,"title":["Domain-free pure type systems"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Morten Heine","family":"S\u00d8rensen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"S. van Bakel, L. Liquori, S. Ronchi della Roncha, and P. Urzyczyn. Comparing cubes. In A. Nerode and Y.N. Matiyasevich, editors, Proceedings of LFCS'94, volume 813 of Lecture Notes in Computer Science, pages 353\u2013365. Springer-Verlag, 1994. An extended version is to appear in Annals of Pure and Applied Logic.","DOI":"10.1007\/3-540-58140-5_33"},{"issue":"2","key":"2_CR2","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"H. Barendregt. Introduction to Generalised Type Systems. J. Functional Programming, 1(2):125\u2013154, April 1991.","journal-title":"J. Functional Programming"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, pages 117\u2013309. Oxford Science Publications, 1992. Volume 2.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"2_CR4","unstructured":"G. Barthe, J. Hatcliff, and M.H. S\u00d8rensen. CPS-translation and applications: the cube and beyond. In O. Danvy, editor, Proc. of the 2nd ACM SIGPLAN Workshop on Continuations, number NS-96-13 in BRICS Notes, pages 4:1\u201331, 1996."},{"key":"2_CR5","unstructured":"G. Barthe, J. Hatcliff, and M.H. S\u00d8rensen. Classical pure type systems. In Proceedings of MFPS'97, Electronic Notes in Theoretical Computer Science, 1997."},{"key":"2_CR6","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR7","doi-asserted-by":"crossref","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"H. Curry","year":"1934","unstructured":"H. Curry. Functionality in combinatory logic. Proceedings of the National Academy of Science USA, 20:584\u2013590, 1934.","journal-title":"Proceedings of the National Academy of Science USA"},{"key":"2_CR8","unstructured":"H. Geuvers. Logics and type systems. PhD thesis, University of Nijmegen, 1993."},{"key":"2_CR9","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers and M.-J. Nederhof. A modular proof of strong normalisation for the Calculus of Constructions. Journal of Functional Programming, 1:155\u2013189, 1991.","journal-title":"Journal of Functional Programming"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"H. Geuvers and B. Werner. On the Church-Rosser property for expressive type systems and its consequence for their metatheoretic study. In Proceedings of LICS'94, pages 320\u2013329. IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316057"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"P. Giannini and S. Ronchi Della Rocca. Characterization of typings in polymorphic type discipline. In Proceedings of LICS'88, pages 61\u201370. IEEE Computer Society Press, 1988.","DOI":"10.1109\/LICS.1988.5101"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"D. Leivant. Polymorphic type inference. In Proceedings of POPL'83, pages 88\u201398. ACM Press, 1983.","DOI":"10.1145\/567067.567077"},{"key":"2_CR13","unstructured":"L. Magnusson. The implementation of ALF: a proof editor based on Martin-L\u00f6f's monomorphic type theory with explicit substitution. PhD thesis, Department of Computer Science, Chalmers University, 1994."},{"key":"2_CR14","unstructured":"P. Severi. Normalisation in lambda calculus and its relation to type inference. PhD thesis, Department of Computer Science, Technical University of Eindhoven, 1996."},{"issue":"1","key":"2_CR15","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1996.2622","volume":"133","author":"M.H. S\u00d8rensen","year":"1997","unstructured":"M.H. S\u00d8rensen. Strong normalization from weak normalization in typed \u03bb-calculi. Information and Computation, 133(1):35\u201371, 1997.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63045-7_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T18:01:45Z","timestamp":1713636105000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63045-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540630456","9783540690658"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-63045-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}