{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:00:21Z","timestamp":1725487221792},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672579"},{"type":"electronic","value":"9783540464327"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46432-8_5","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:22:02Z","timestamp":1184588522000},"page":"63-81","source":"Crossref","is-referenced-by-count":6,"title":["Proof Nets and Explicit Substitutions"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Di Cosmo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emmanuel","family":"Polonovski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,5,19]]},"reference":[{"issue":"1","key":"5_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"4","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P. L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 4(1):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"S. Abramsky and R. Jagadeesan. New foundations for the geometry of interaction. In Proc. of LICS, pages 211\u2013222, 1992.","DOI":"10.1109\/LICS.1992.185534"},{"key":"5_CR3","unstructured":"R. Bloo. Preservation of Termination for Explicit Substitution. PhD thesis, Eindhoven University of Technology, 1997."},{"key":"5_CR4","unstructured":"R. Bloo and K. Rose. Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. In Computing Science in the Netherlands, pages 62\u201372. Netherlands Computer Science Research Foundation, 1995."},{"key":"5_CR5","unstructured":"V. Danos. La logique lin\u00e9aire appliqu\u00e9e \u00e0 l\u2019\u00e9tude de divers processus de normalisation (et principalement du \u03bb-calcul). PhD thesis, Universit\u00e9 de Paris VII, 1990. Th\u00e8se de doctorat de math\u00e9matiques."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"V. Danos, J.-B. Joinet, and H. Schellinx. Sequent calculi for second order logic. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic. Cambridge University Press, 1995.","DOI":"10.1017\/CBO9780511629150.011"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"V. Danos and L. Regnier. Proof-nets and the Hilbert space. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 307\u2013328. Cambridge University Press, London Mathematical Society Lecture Notes, 1995.","DOI":"10.1017\/CBO9780511629150.016"},{"key":"5_CR8","unstructured":"R. David and B. Guillaume. The \u03bb l-calculus. In Proceedigs of WESTAPP, pages 2\u201313, Trento, Italy, 1999."},{"key":"5_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-48685-2_6","volume-title":"Proc of RTA","author":"R. Cosmo Di","year":"1999","unstructured":"R. Di Cosmo and S. Guerrini. Strong normalization of proof nets modulo structural congruences. In P. Narendran and M. Rusinowitch, editors, Proc of RTA, volume 1631 of LNCS, pages 75\u201389, Trento, Italy, 1999. Springer Verlag."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D. Kesner. Strong normalization of explicit substitutions via cut elimination in proof nets. In Proc of LICS, pages 35\u201346, Warsaw, Poland, 1997.","DOI":"10.1109\/LICS.1997.614927"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo, D. Kesner, and E. Polonovski. Proof nets and explicit substitutions. Technical report, LRI, Universit\u00e9 Paris-Sud, 2000. Available as ftp:\/\/ftp.lri.fr\/LRI\/articles\/kesner\/es-pn.ps.gz .","DOI":"10.1007\/3-540-46432-8_5"},{"issue":"4","key":"5_CR12","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s002000050110","volume":"9","author":"M. C. Ferreira","year":"1999","unstructured":"M. C. Ferreira, D. Kesner, and L. Puel. Lambda-calculi with explicit substitutions preserving strong normalization. Applicable Algebra in Engineering Communication and Computing, 9(4):333\u2013371, 1999.","journal-title":"Applicable Algebra in Engineering Communication and Computing"},{"issue":"1","key":"5_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1\u2013101, 1987.","journal-title":"Theoretical Computer Science"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Geometry of interaction I: interpretation of system F. In R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo, editors, Logic colloquium 1988, pages 221\u2013260. North Holland, 1989.","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"G. Gonthier, M. Abadi, and J.-J. L\u00e9vy. The geometry of optimal lambda reduction. In Proc. of POPL, pages 15\u201326, Albuquerque, New Mexico, 1992. ACM Press.","DOI":"10.1145\/143165.143172"},{"key":"5_CR16","unstructured":"B. Guillaume. Un calcul de substitution avec \u00c9tiquettes. PhD thesis, Universit\u00e9 de Savoie, 1999."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"J. Lamping. An algorithm for optimal lambda calculus reduction. In Proc. of POPL, pages 16\u201330, San Francisco, California, 1990. ACM Press.","DOI":"10.1145\/96709.96711"},{"key":"5_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Proc of TLCA","author":"P.-A. Melli\u00e8s","year":"1995","unstructured":"P.-A. Melli\u00e8s. Typed \u03bb-calculi with explicit substitutions may not terminate. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proc of TLCA, volume 902 of LNCS, April 1995."},{"key":"5_CR19","series-title":"Lect Notes Comput Sci","first-page":"36","volume-title":"Proc. of CTRS","author":"K. Rose","year":"1992","unstructured":"K. Rose. Explicit cyclic substitutions. In Rusinowitch and R\u00e9my, editors, Proc. of CTRS, number 656 in LNCS, pages 36\u201350, 1992."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46432-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:32:37Z","timestamp":1556667157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46432-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672579","9783540464327"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-46432-8_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}