{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:56:36Z","timestamp":1725562596754},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221647"},{"type":"electronic","value":"9783540248491"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_15","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T16:34:24Z","timestamp":1281285264000},"page":"226-241","source":"Crossref","is-referenced-by-count":1,"title":["Classical Proofs, Typed Processes, and Intersection Types"],"prefix":"10.1007","author":[{"given":"Silvia","family":"Ghilezan","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Lescanne","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"15_CR1","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0025","volume":"125","author":"F. Barbanera","year":"1996","unstructured":"Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Information and Computation\u00a0125(2), 103\u2013117 (1996)","journal-title":"Information and Computation"},{"key":"15_CR2","volume-title":"The Lambda Calculus: its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984) (revised edition)"},{"issue":"1","key":"15_CR3","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1017\/S0956796899003524","volume":"10","author":"H.P. Barendregt","year":"2000","unstructured":"Barendregt, H.P., Ghilezan, S.: Lambda terms for natural deduction, sequent calculus and cut-elimination. Journal of Functional Programming\u00a010(1), 121\u2013134 (2000)","journal-title":"Journal of Functional Programming"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1017\/S0960129500003248","volume":"1","author":"E. Bonelli","year":"2001","unstructured":"Bonelli, E.: Perpetuality in a named lambda calculus with explicit substitutions. Mathematical Structures in Computer Science\u00a01, 47\u201390 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF02011875","volume":"19","author":"M. Coppo","year":"1978","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: A new type-assignment for lambda terms. Archiv f\u00fcr Mathematische Logik\u00a019, 139\u2013156 (1978)","journal-title":"Archiv f\u00fcr Mathematische Logik"},{"issue":"4","key":"15_CR6","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the \u03bb-calculus. Notre Dame Journal of Formal Logic\u00a021(4), 685\u2013693 (1980)","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"15_CR7","first-page":"535","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"M. Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Principal type schemes and \u03bb-calculus semantics. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 535\u2013560. Academic Press, London (1980)"},{"key":"15_CR8","volume-title":"Proceedings of the 5th ACMSIGPLAN International Conference on Functional Programming (ICFP 2000)","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Proceedings of the 5th ACMSIGPLAN International Conference on Functional Programming (ICFP 2000), Montreal, Canada, ACM Press, New York (2000)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-45413-6_13","volume-title":"Typed Lambda Calculi and Applications","author":"D. Dougherty","year":"2001","unstructured":"Dougherty, D., Lescanne, P.: Reductions, intersection types, and explicit substitution. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 121\u2013135. Springer, Heidelberg (2001)"},{"key":"15_CR10","series-title":"Translation of Mathematical Monographs","doi-asserted-by":"crossref","DOI":"10.1090\/mmono\/067","volume-title":"Mathematical Intuitionism","author":"D. Dragalin","year":"1988","unstructured":"Dragalin, D.: Mathematical Intuitionism. Translation of Mathematical Monographs, vol.\u00a067. American Mathematical Society, Providence (1988)"},{"unstructured":"Herbelin, H.: S\u00e9quents qu\u2019on calcule: de l\u2019interpr\u00e9tation du calcul des s\u00e9quents comme calcul de \u03bb-termes et comme calcul de strat\u00e9gies gagnantes. Th\u00e8se d\u2019universit\u00e9, Universit\u00e9 Paris 7 (Janvier 1995)","key":"15_CR11"},{"issue":"3","key":"15_CR12","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1093\/logcom\/11.3.431","volume":"11","author":"H. Herbelin","year":"2001","unstructured":"Herbelin, H.: Explicit substitution and reducibility. Journal of Logic and Computation\u00a011(3), 431\u2013451 (2001)","journal-title":"Journal of Logic and Computation"},{"issue":"1-2","key":"15_CR13","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0304-3975(83)90074-9","volume":"28","author":"J.R. Hindley","year":"1984","unstructured":"Hindley, J.R.: Coppo\u2013Dezani types do not correspond to propositional logic. Theoretical Computer Science\u00a028(1-2), 235\u2013236 (1984)","journal-title":"Theoretical Computer Science"},{"key":"15_CR14","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A.: The formulas-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479\u2013490. Academic Press, London (1980)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"issue":"4","key":"15_CR16","doi-asserted-by":"publisher","first-page":"1461","DOI":"10.2307\/2275652","volume":"62","author":"M. Parigot","year":"1997","unstructured":"Parigot, M.: Proofs of strong normalisation for second order classical natural deduction. The Journal of Symbolic Logic\u00a062(4), 1461\u20131479 (1997)","journal-title":"The Journal of Symbolic Logic"},{"key":"15_CR17","first-page":"561","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"G. Pottinger","year":"1980","unstructured":"Pottinger, G.: A type assignment for the strongly normalizable \u03bb-terms. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561\u2013577. Academic Press, London (1980)"},{"unstructured":"Rees, J.A.: A security kernel based on the lambda calculus. A.I. Memo 1564, Massachusetts Institute of Technology (March 1996)","key":"15_CR18"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/3-540-08860-1_30","volume-title":"Automata, Languages and Programming","author":"P. Sall\u00e9","year":"1978","unstructured":"Sall\u00e9, P.: Une extension de la th\u00e9orie des types en lambda-calcul. In: Ausiello, G., B\u00f6hm, C. (eds.) ICALP 1978. LNCS, vol.\u00a062, pp. 398\u2013410. Springer, Heidelberg (1978)"},{"unstructured":"Wadler, P.: Proofs are programs: 19th century logic and 21st century computing, available as \n                  \n                    http:\/\/www.research.avayalabs.com\/user\/wadler\/topics\/history.html","key":"15_CR20"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T21:41:40Z","timestamp":1578519700000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_15"}},"subtitle":["Extended Abstract"],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}