{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T23:05:25Z","timestamp":1779145525052,"version":"3.51.4"},"reference-count":40,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T00:00:00Z","timestamp":1669075200000},"content-version":"unspecified","delay-in-days":82,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper studies normalisation by evaluation for typed lambda calculus from a categorical and algebraic viewpoint. The first part of the paper analyses the lambda definability result of Jung and Tiuryn via Kripke logical relations and shows how it can be adapted to unify definability and normalisation, yielding an extensional normalisation result. In the second part of the paper, the analysis is refined further by considering intensional Kripke relations (in the form of Artin\u2013Wraith glueing) and shown to provide a function for normalising terms, casting normalisation by evaluation in the context of categorical glueing. The technical development includes an algebraic treatment of the syntax and semantics of the typed lambda calculus that allows the definition of the normalisation function to be given within a simply typed metatheory. A normalisation-by-evaluation program in a dependently typed functional programming language is synthesised.<\/jats:p>","DOI":"10.1017\/s0960129522000263","type":"journal-article","created":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T12:05:09Z","timestamp":1669118709000},"page":"1028-1065","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":6,"title":["Semantic analysis of normalisation by evaluation for typed lambda calculus"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8558-3492","authenticated-orcid":false,"given":"Marcelo","family":"Fiore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2022,11,22]]},"reference":[{"key":"S0960129522000263_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00283-O"},{"key":"S0960129522000263_ref36","unstructured":"Streicher, T. (1998). Categorical intuitions underlying semantic normalisation proofs. In: Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation (NBE\u201998), BRICS Note NS-98-8. Department of Computer Science, University of Aarhus, 9\u201310."},{"key":"S0960129522000263_ref33","unstructured":"Plotkin, G. (1973). Lambda-definability and logical relations. Technical report, School of Artificial Intelligence, University of Edinburgh."},{"key":"S0960129522000263_ref3","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932506"},{"key":"S0960129522000263_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70727-4"},{"key":"S0960129522000263_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_32"},{"key":"S0960129522000263_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/10704567_23"},{"key":"S0960129522000263_ref18","doi-asserted-by":"crossref","unstructured":"Filinski, A. (2001). Normalization by evaluation for the computational lambda-calculus. In: Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, Springer-Verlag.","DOI":"10.1007\/3-540-45413-6_15"},{"key":"S0960129522000263_ref25","unstructured":"Girard, J.-Y. (1972). Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de doctorat d\u2019\u00e9tat, Universit\u00e9 Paris 7."},{"key":"S0960129522000263_ref38","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"S0960129522000263_ref34","unstructured":"Reynolds, J. (1998). Normalization and functor categories. In: Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation (NBE\u201998), BRICS Note NS-98-8. Department of Computer Science, University of Aarhus, 33\u201336."},{"key":"S0960129522000263_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(74)90014-0"},{"key":"S0960129522000263_ref10","doi-asserted-by":"crossref","unstructured":"Bezem, M. and Groote, J. (eds.) (1993). Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 664, Springer, Springer-Verlag.","DOI":"10.1007\/BFb0037093"},{"key":"S0960129522000263_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_27"},{"key":"S0960129522000263_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129596002150"},{"key":"S0960129522000263_ref28","volume-title":"Cambridge Studies in Advanced Mathematics","volume":"7","author":"Lambek","year":"1986"},{"key":"S0960129522000263_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172707"},{"key":"S0960129522000263_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964007"},{"key":"S0960129522000263_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002508"},{"key":"S0960129522000263_ref11","unstructured":"Coquand, C. (1994). From semantics to rules: A machine assisted analysis. In: B\u00f6rger, E., Gurevich, Y. and Meinke, K. (eds.) Proceedings of the Computer Science Logic\u201993, Lecture Notes in Computer Science, vol. 832, Springer-Verlag."},{"key":"S0960129522000263_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/BF01752392"},{"key":"S0960129522000263_ref27","unstructured":"Krivine, J. (1993). Lambda-Calculus, Types and Models, Computers and their Applications, Masson and Ellis Horwood."},{"key":"S0960129522000263_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_12"},{"key":"S0960129522000263_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"S0960129522000263_ref39","volume-title":"Cambridge Studies in Advanced Mathematics","volume":"59","author":"Taylor","year":"1999"},{"key":"S0960129522000263_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037110"},{"key":"S0960129522000263_ref24","unstructured":"O\u2019Caml, Fresh . In: www.cl.cam.ac.uk\/ amp12\/fresh-ocaml\/."},{"key":"S0960129522000263_ref15","doi-asserted-by":"crossref","unstructured":"Danvy, O. (1998). Type-directed partial evaluation. In: Partial Evaluation \u2014 Practise and Theory, Proceedings of the 1998 DIKU Summer School, Lecture Notes in Computer Science, vol. 1706, Springer-Verlag, 367\u2013411.","DOI":"10.1007\/3-540-47018-2_16"},{"key":"S0960129522000263_ref23","doi-asserted-by":"crossref","unstructured":"Fiore, M. and Szamozvancev, D. (2022). Formal metatheory of second-order abstract syntax. In: Proceedings of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022).","DOI":"10.1145\/3498715"},{"key":"S0960129522000263_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037100"},{"key":"S0960129522000263_ref20","doi-asserted-by":"crossref","unstructured":"Fiore, M. and Hur, C.-K. (2010). Second-order equational logic. In: Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010), Lecture Notes in Computer Science, vol. 6247, Springer-Verlag, 320\u2013335.","DOI":"10.1007\/978-3-642-15205-4_26"},{"key":"S0960129522000263_ref32","doi-asserted-by":"crossref","unstructured":"Pfenning, F. and Elliot, C. (1988). Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN\u201988 Symposium on Language Design and Implementation.","DOI":"10.1145\/53990.54010"},{"key":"S0960129522000263_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"S0960129522000263_ref21","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"S0960129522000263_ref30","first-page":"1","volume-title":"Computer Science","volume":"598","author":"Ma","year":"1992"},{"key":"S0960129522000263_ref16","unstructured":"Danvy, O. and Dybjer, P. (eds.) (1998). Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation (NBE\u201998), BRICS Note NS-98-8. Department of Computer Science, University of Aarhus."},{"key":"S0960129522000263_ref9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151645"},{"key":"S0960129522000263_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000076"},{"key":"S0960129522000263_ref37","first-page":"288","volume-title":"Electronic Notes in Theoretical Computer Science","volume":"29","author":"Streicher","year":"2000"},{"key":"S0960129522000263_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000263","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,5]],"date-time":"2023-04-05T02:00:05Z","timestamp":1680660005000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000263\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9]]},"references-count":40,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2022,9]]}},"alternative-id":["S0960129522000263"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000263","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,9]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}