{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:40:18Z","timestamp":1725496818917},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665366"},{"type":"electronic","value":"9783540481683"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"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":[[1999]]},"DOI":"10.1007\/3-540-48168-0_15","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T06:30:26Z","timestamp":1196490626000},"page":"204-219","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Using Fields and Explicit Substitutions to Implement Objects and Functions in a de Bruijn Setting"],"prefix":"10.1007","author":[{"given":"Eduardo","family":"Bonelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Cardelli. A Theory of Objects. Springer Verlag, 1996.","DOI":"10.1007\/978-1-4419-8598-9"},{"issue":"1","key":"15_CR2","first-page":"375","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":"Explicit Substitutions"},{"key":"15_CR3","unstructured":"R. Bloo. Preservation of Termination for Explicit Substitution. PhD. Thesis, Eindhoven University, 1997."},{"key":"15_CR4","unstructured":"R. Bloo and H. Geuvers. Explicit Substitution: on the edge of strong normalization. Theoretical Computer Science, 204, 1998."},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"R. Bloo, K. Rose. Combinatory Reduction Systems with explicit substitution that preserve strong normalization. In RTA\u201996, LNCS 1103, 1996.","DOI":"10.1007\/3-540-61464-8_51"},{"key":"15_CR6","unstructured":"E. Bonelli. Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting. Full version obtainable by ftp at \nftp:\/\/ftp.lri.fr\/LRI\/articles\/bonelli\/objectdbfull.ps.gz\n\n."},{"key":"15_CR7","series-title":"Lect Notes Comput Sci","volume-title":"An explicit eta rewrite rule","author":"D. Briaud","year":"1995","unstructured":"D. Briaud. An explicit eta rewrite rule. In M. Dezani Ed., Int. Conference on Typed Lambda Calculus and Applications, LNCS vol. 902, 1995."},{"key":"15_CR8","first-page":"381","volume":"75","author":"N.G. Bruijn de","year":"1972","unstructured":"N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formual manipulation with application to the Church-Rosser theorem. Koninklijke Nederlandse Akademie van Wetenschappen, Series A, Mathematical Sciences, 75:381\u2013392, 1972.","journal-title":"Lambda calculus notation with nameless dummies, a tool for automatic formual manipulation with application to the Church-Rosser theorem"},{"key":"15_CR9","volume-title":"Confluence properties of weak and strong calculi of explicit substitutions","author":"P.-L. Curien","year":"1991","unstructured":"P.-L. Curien, T. Hardin, and J.-J. L\u00e9vy. Confluence properties of weak and strong calculi of explicit substitutions. Technical Report, Centre d\u2019Etudes et de Recherche en Informatique, CNAM, 1991."},{"issue":"3","key":"15_CR10","first-page":"279","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279\u2013301, 1982.","journal-title":"Orderings for term rewriting systems"},{"key":"15_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Lambda-calculi with explicit substitutions and composition which preserve beta-strong normalization","author":"M. Ferreira","year":"1996","unstructured":"M. Ferreira, D. Kesner. and L. Puel. Lambda-calculi with explicit substitutions and composition which preserve beta-strong normalization. Proceedings of the 5th International Conference on Algebraic and Logic Programming (ALP\u201996), LNCS 1139, 1996."},{"key":"15_CR12","unstructured":"T. Hardin. R\u00e9sultats de confluence pour les r\u00e8gles fortes de la logique combinatoire cat\u00e9gorique et liens avec les lambda-calculs. Th\u00e8se de doctorat, Universit\u00e9 de Paris VII, 1987."},{"key":"15_CR13","unstructured":"T. Hardin and J-J. L\u00e9vy. A confluent calculus of substitutions. In France-Japan Artificial Intelligence and Computer Science Symposium, 1989."},{"key":"15_CR14","series-title":"Lect Notes Comput Sci","volume-title":"A lambda calculus a la de Bruijn with Explicit Substitutions","author":"F. Kamareddine","year":"1995","unstructured":"F. Kamareddine and A. R\u00edos. A lambda calculus a la de Bruijn with Explicit Substitutions. Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs (PLILP\u201995), LNCS 982, 1995."},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"F. Kamareddine and A. R\u00edos. Extending a \u03bb-calculus with Explicit Substitutions which Preserves Strong Normalization into a Confluent Calculus on Open Terms. In Journal of Functional Programming, Vol.7 No.4, 1997.","DOI":"10.1017\/S0956796897002785"},{"key":"15_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Confluence properties of extensional and non-extensional lambda-calculi with explicit substitutions","author":"D. Kesner","year":"1996","unstructured":"D. Kesner. Confluence properties of extensional and non-extensional lambda-calculi with explicit substitutions. Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA\u201996), LNCS 1103, 1996."},{"key":"15_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/BFb0056615","volume-title":"Explicit Substitutions for Objects and Functions","author":"D. Kesner","year":"1998","unstructured":"D. Kesner, P.E. Mart\u00ednez L\u00f3pez. Explicit Substitutions for Objects and Functions. Proceedings of the Joint International Symposiums: Programming Languages, Implementations, Logics and Program (PLILP\u201998) and Algebraic and Logic Programming (ALP), LNCS 1490,pp. 195\u2013212, Sept. 1998."},{"key":"15_CR18","unstructured":"J.W. Klop. Combinatory Reduction Systems. PhD Thesis, University of Utrecht, 1980."},{"key":"15_CR19","unstructured":"J.W. Klop. Term Rewriting Systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, Volume II, Oxford University Press, 1992."},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"P. Lescanne. From \u03bb\n\u03c3to \u03bb\n\u03bd, a journey through calculi of explicit substitutions. In Ann. ACM Symp. on Principles of Programming Languages (POPL), pp. 60\u201369. ACM, 1994.","DOI":"10.1145\/174675.174707"},{"key":"15_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Explicit substitutions with de Bruijn\u2019s levels","author":"P. Lescanne","year":"1995","unstructured":"P. Lescanne and J. Rouyer Degli. Explicit substitutions with de Bruijn\u2019s levels. In P. Lescanne editor, RTA\u201995, LNCS 914, 1995."},{"key":"15_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Typed \u03bb-calculi with explicit substitutions may not terminate","author":"P.A. Melli\u00e8s","year":"1995","unstructured":"P.A. Melli\u00e8s. Typed \u03bb-calculi with explicit substitutions may not terminate. In TLCA\u201995, LNCS 902, 1995."},{"key":"15_CR23","unstructured":"C.A. Mu\u00f1oz. Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus. Proceedings of the Eleven Annual IEEE Symposium on Logic in Computer Science, 1996."},{"key":"15_CR24","unstructured":"B. Pagano. Des calculs de substitution explicit et leur application \u00e0 la compilation des langages fonctionnels. Th\u00e8se de doctorat, Universit\u00e9 de Paris VII, 1998."},{"key":"15_CR25","unstructured":"A. R\u00edos. Contribution \u00e0 l\u2019\u00e9tude des \u03bb-calculs avec substitutions explicites. Ph.D Thesis, Universit\u00e9 de Paris VII, 1993."},{"key":"15_CR26","series-title":"Lect Notes Comput Sci","volume-title":"Explicit Cyclic Substitutions","author":"K. Rose","year":"1992","unstructured":"K. Rose. Explicit Cyclic Substitutions. In CTRS\u201992, LNCS 656, 1992."},{"key":"15_CR27","first-page":"113","volume":"7","author":"M. Takahashi","year":"1989","unstructured":"M. Takahashi. Parallel reduction in the \u03bb-calculus. Journal of Symbolic Computation, 7:113\u2013123, 1989.","journal-title":"Parallel reduction in the \u03bb-calculus"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48168-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T00:08:35Z","timestamp":1586131715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"13 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}