{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:32:55Z","timestamp":1725485575147},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"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":[[2002]]},"DOI":"10.1007\/3-540-36078-6_9","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:48:36Z","timestamp":1180666116000},"page":"130-144","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Binding Logic: Proofs and Models"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Th\u00e9r\u00e8se","family":"Hardin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"issue":"4","key":"9_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, J.-J. L\u00e9vy, Explicit substitutions, Journal of Functional Programming, 1,4 (1991) pp. 375\u2013416.","journal-title":"Journal of Functional Programming"},{"key":"9_CR2","unstructured":"P.B. Andrews, An introduction to mathematical logic and type theory: to truth through proof, Academic Press (1986)."},{"key":"9_CR3","unstructured":"A. Barber, Dual Intuitionistic Linear Logic, Technical Report ECS-LFCS-96-347, University of Edinburgh (1996)."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"N.G. de Bruijn, 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.","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"P.-L. Curien, Categorical combinators, sequential algorithms and functional programming, Birkhauser (1993).","DOI":"10.1007\/978-1-4612-0317-9"},{"issue":"2","key":"9_CR6","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.-L. Curien","year":"1996","unstructured":"P.-L. Curien, Th. Hardin and J.-J. L\u00e9vy, Weak and strong confluent calculi of explicit substitutions, Journal of the ACM, 43,2 (1996) pp. 362\u2013397.","journal-title":"Journal of the ACM"},{"key":"9_CR7","volume-title":"Combinatory Logic, I","author":"H.B. Curry","year":"1958","unstructured":"H.B. Curry, R. Feys, Combinatory Logic, I, North Holland, Amsterdam (1958)."},{"key":"9_CR8","unstructured":"G. Dowek, La part du calcul, M\u00e9moire d\u2019Habilitation \u00e0 Diriger des Recherches, Universit\u00e9 de Paris VII (1999)."},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G. Dowek","year":"2000","unstructured":"G. Dowek, Th. Hardin and C. Kirchner, Higher-order unification via explicit substitutions, Information and Computation, 157 (2000) pp. 183\u2013235.","journal-title":"Information and Computation"},{"key":"9_CR10","unstructured":"G. Dowek, Th. Hardin and C. Kirchner, Theorem proving modulo, Rapport de Recherche 3400, INRIA (1998). To appear in Journal of Automated Reasonning."},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0960129500003236","volume":"11","author":"G. Dowek","year":"2001","unstructured":"G. Dowek, Th. Hardin and C. Kirchner, HOL-lambda-sigma: an intensional first-order expression of higher-order logic, Mathematical Structures in Computer Science, 11 (2001) pp. 1\u201325.","journal-title":"Mathematical Structures in Computer Science"},{"key":"9_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-48167-2_5","volume-title":"Types for Proofs and Programs","author":"G. Dowek","year":"1999","unstructured":"G. Dowek and B. Werner, Proof normalization modulo, Types for Proofs and Programs 98, T. Altenkirch, W. Naraschewski, B. Rues (Eds.), Lecture Notes in Computer Science 1657, Springer-Verlag (1999), pp. 62\u201377."},{"key":"9_CR13","unstructured":"M. Fiore, G. Plotkin, and D. Turi, Abstract syntax and variable binding, Logic in Computer Science (1999) pp. 193\u2013202."},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"L. Henkin, Completeness in the theory of types, The Journal of Symbolic Logic, 15 (1950) pp. 81\u201391.","journal-title":"The Journal of Symbolic Logic"},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1002\/malq.19770230708","volume":"23","author":"J.R. Hindley","year":"1977","unstructured":"J.R. Hindley, Combinatory reductions and lambda reductions compared, Zeit. Math. Logik, 23 (1977) pp. 169\u2013180.","journal-title":"Zeit. Math. Logik"},{"key":"9_CR16","unstructured":"J. Lambek, Deductive systems and categories II. Standard constructions and closed categories. Category theory, homology theory and their applications I, Lecture Notes in Mathematics, 86, Springer-Verlag (1969) pp. 76\u2013122."},{"key":"9_CR17","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1090\/conm\/092\/1003201","volume":"92","author":"J. Lambek","year":"1989","unstructured":"J. Lambek, Multicategories revisited, Contemporary Mathematics, 92 (1989) 217\u2013239.","journal-title":"Contemporary Mathematics"},{"key":"9_CR18","unstructured":"D. Miller and G. Nadathur, A logic programming approach to manipulating formulas and programs. Symposium on Logic Programming (1987)."},{"key":"9_CR19","unstructured":"B. Pagano, X.R.S: eXplicit Reduction Systems, a first-order calculus for higher-order calculi, Conference on Automated Deduction, C. Kirchner and H. Kirchner (Eds.), LNAI 1421, Springer-Verlag (1998), pp. 72\u201388."},{"key":"9_CR20","unstructured":"B. Pagano, Des calculs de substitution explicites et de leur application a la compilation des langages fonctionnels. Th\u00e9se de Doctorat, Universit\u00e9 de Paris VI (1998)."},{"key":"9_CR21","unstructured":"F. Pfenning and C. Elliott, Higher-order abstract syntax, Conference on Programming Language Design and Implementation, ACM Press, (1988) pp. 199\u2013208."},{"key":"9_CR22","unstructured":"S. Vaillant, Expressing set theory in first-order predicate logic, International Workshop on Explicit Substitutions Theory and Applications to Programs and Proofs (2000)."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:27:35Z","timestamp":1558272455000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"24 October 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}