{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:15:11Z","timestamp":1767928511896,"version":"3.49.0"},"reference-count":118,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2019,12,10]],"date-time":"2019-12-10T00:00:00Z","timestamp":1575936000000},"content-version":"unspecified","delay-in-days":343,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks.<\/jats:p>","DOI":"10.1017\/s0956796819000170","type":"journal-article","created":{"date-parts":[[2019,12,10]],"date-time":"2019-12-10T02:51:55Z","timestamp":1575946315000},"source":"Crossref","is-referenced-by-count":25,"title":["POPLMark reloaded: Mechanizing proofs by logical relations"],"prefix":"10.1017","volume":"29","author":[{"given":"ANDREAS","family":"ABEL","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4091-657X","authenticated-orcid":false,"given":"GUILLAUME","family":"ALLAIS","sequence":"additional","affiliation":[]},{"given":"ALIYA","family":"HAMEER","sequence":"additional","affiliation":[]},{"given":"BRIGITTE","family":"PIENTKA","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0942-4777","authenticated-orcid":false,"given":"ALBERTO","family":"MOMIGLIANO","sequence":"additional","affiliation":[]},{"given":"STEVEN","family":"SCH\u00c4FER","sequence":"additional","affiliation":[]},{"given":"KATHRIN","family":"STARK","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2019,12,10]]},"reference":[{"key":"S0956796819000170_ref118","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_25"},{"key":"S0956796819000170_ref117","unstructured":"Werner, B. (1992) A normalization proof for an impredicative type system with large elimination over integers. In International Workshop on Types for Proofs and Programs (TYPES), pp. 341\u2013357."},{"key":"S0956796819000170_ref116","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034818"},{"key":"S0956796819000170_ref115","doi-asserted-by":"publisher","DOI":"10.21236\/ADA418517"},{"key":"S0956796819000170_ref114","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505889"},{"key":"S0956796819000170_ref113","unstructured":"van Raamsdonk, F. & Severi, P. (1995) On Normalisation. Technical report 95\/20. Technische Universiteit Eindhoven."},{"key":"S0956796819000170_ref111","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:14)2012"},{"key":"S0956796819000170_ref110","doi-asserted-by":"publisher","DOI":"10.1145\/1656242.1656248"},{"key":"S0956796819000170_ref108","unstructured":"Sturm, S. (2018) Verification and Theorem Proving in F*. M.Phil. thesis, LMU. https:\/\/github.com\/sturmsebastian\/Fstar-master-thesis-code."},{"key":"S0956796819000170_ref107","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.44"},{"key":"S0956796819000170_ref106","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693163"},{"key":"S0956796819000170_ref105","unstructured":"Sch\u00e4fer, S. , Tebbi, T. & Smolka, G. (2014) Autosubst: Automation for de Bruijn substitutions. In 6th Coq Workshop, July 2014."},{"key":"S0956796819000170_ref104","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"S0956796819000170_ref103","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_31"},{"key":"S0956796819000170_ref99","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58085-9_82"},{"key":"S0956796819000170_ref98","unstructured":"Plotkin, G. (1973) Lambda-Definability and Logical Relations. Memorandum sai-rm-4. University of Edinburgh."},{"key":"S0956796819000170_ref45","unstructured":"Crary, K. (2005) Logical relations and a case study in equivalence checking. In Advanced Topics in Types and Programming Languages, Pierce, B. C. (ed). MIT."},{"key":"S0956796819000170_ref86","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000415"},{"key":"S0956796819000170_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55808-X_19"},{"key":"S0956796819000170_ref44","unstructured":"Coquand, C. (1993) From semantics to rules: A machine assisted analysis. In Computer Science Logic, 7th Workshop, CSL\u201993, Swansea, United Kingdom, September 13\u201317, 1993, Selected Papers , B\u00f6rger, E. , Gurevich, Y. & Meinke, K. (eds), Lecture Notes in Computer Science, vol. 832. Springer, pp. 91\u2013105."},{"key":"S0956796819000170_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1088454.1088459"},{"key":"S0956796819000170_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"S0956796819000170_ref22","first-page":"1","article-title":"Normalisation by evaluation for type theory, in type theory","volume":"13","author":"Altenkirch","year":"2017","journal-title":"Logical Methods Comput. Sci."},{"key":"S0956796819000170_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_5"},{"key":"S0956796819000170_ref36","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000154"},{"key":"S0956796819000170_ref42","first-page":"311","article-title":"\u03b1 check: A mechanized metatheory model checker","volume":"17","author":"Cheney","year":"2017","journal-title":"TPLP"},{"key":"S0956796819000170_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103705"},{"key":"S0956796819000170_ref26","unstructured":"Aydemir, B. & Weirich, S. (2010) LNgen: Tool Support for Locally Nameless Representations. Technical report. MS-CIS-10-24. University of Pennsylvania."},{"key":"S0956796819000170_ref76","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190245"},{"key":"S0956796819000170_ref89","first-page":"230","volume-title":"AFP Summer School.","author":"Norell","year":"2009"},{"key":"S0956796819000170_ref28","first-page":"265","article-title":"Universes for generic programs and proofs in dependent type theory","volume":"10","author":"Benke","year":"2003","journal-title":"Nordic J. Comput."},{"key":"S0956796819000170_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"S0956796819000170_ref72","doi-asserted-by":"publisher","DOI":"10.1145\/3130261.3130263"},{"key":"S0956796819000170_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_8"},{"key":"S0956796819000170_ref4","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.43.2"},{"key":"S0956796819000170_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S0956796819000170_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"S0956796819000170_ref82","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90023-7"},{"key":"S0956796819000170_ref14","unstructured":"Allais, G. , Atkey, R. , Chapman, J. , McBride, C. & McKinna, J. (2018). A type and scope safe universe of syntaxes with binding: Their semantics and proofs. Proc. ACM Program. Lang. 2(ICFP), 90:1\u201390:30."},{"key":"S0956796819000170_ref19","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:3)2015"},{"key":"S0956796819000170_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/1411203.1411226"},{"key":"S0956796819000170_ref71","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-002-0156-9"},{"key":"S0956796819000170_ref37","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2951"},{"key":"S0956796819000170_ref13","first-page":"397","article-title":"A linear language with locations","volume":"77","author":"Ahmed","year":"2007","journal-title":"Fundam. Inform."},{"key":"S0956796819000170_ref35","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.185.3"},{"key":"S0956796819000170_ref97","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9254-5"},{"key":"S0956796819000170_ref59","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_2"},{"key":"S0956796819000170_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35672-3_1"},{"key":"S0956796819000170_ref18","first-page":"1","article-title":"Relative monads formalised","volume":"7","author":"Altenkirch","year":"2014","journal-title":"J. Formalized Reasoning"},{"key":"S0956796819000170_ref100","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863575"},{"key":"S0956796819000170_ref68","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782616"},{"key":"S0956796819000170_ref2","first-page":"1","article-title":"\u2202 for data: Differentiating data structures","volume":"65","author":"Abbott","year":"2005","journal-title":"Fundamenta Informaticae"},{"key":"S0956796819000170_ref85","doi-asserted-by":"publisher","DOI":"10.1145\/2364406.2364411"},{"key":"S0956796819000170_ref96","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0956796819000170_ref3","first-page":"3","volume-title":"Logical Frameworks and Metalanguages (LFM\u201904)","volume":"199","author":"Abel","year":"2008"},{"key":"S0956796819000170_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9327-3"},{"key":"S0956796819000170_ref65","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S0956796819000170_ref10","first-page":"1","volume-title":"Types for Proofs and Programs,","author":"Adams","year":"2006"},{"key":"S0956796819000170_ref83","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"S0956796819000170_ref112","doi-asserted-by":"publisher","DOI":"10.1145\/1877714.1877721"},{"key":"S0956796819000170_ref16","unstructured":"Altenkirch, T. (1992) Brewing Strong Normalization Proof with LEGO. Technical report 92-230. LFCS, Edinburgh. http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/92\/ECS-LFCS-92-230\/ECS-LFCS-92-230.pdf."},{"key":"S0956796819000170_ref61","volume-title":"Proofs and Types","volume":"7","author":"Girard","year":"1989"},{"key":"S0956796819000170_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-006-6604-5"},{"key":"S0956796819000170_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037095"},{"key":"S0956796819000170_ref11","unstructured":"Ahmed, A. (2004) Semantics of Types for Mutable State. Ph.D. thesis, Princeton University."},{"key":"S0956796819000170_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2503887.2503889"},{"key":"S0956796819000170_ref5","first-page":"51","article-title":"Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types","volume":"153","author":"Abel","year":"2014","journal-title":"MSFP"},{"key":"S0956796819000170_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"S0956796819000170_ref12","unstructured":"Ahmed, A. (2013) Logical relations. In Oregon Programming Languages Summer School (OPLSS)."},{"key":"S0956796819000170_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9336-2"},{"key":"S0956796819000170_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_27"},{"key":"S0956796819000170_ref109","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"S0956796819000170_ref24","unstructured":"Anand, A. (2016) Exploiting uniformity in substitution: The Nuprl term model. In The 5th International Congress on Mathematical Software (ICMS 2016)."},{"key":"S0956796819000170_ref64","unstructured":"Group, Nominal Methods (2009) Strong normalization for the simply typed lambda calculus. https:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/HOL-Nominal-Examples\/SN.html."},{"key":"S0956796819000170_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014049"},{"key":"S0956796819000170_ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45213-3_4"},{"key":"S0956796819000170_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"S0956796819000170_ref8","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"S0956796819000170_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"S0956796819000170_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"S0956796819000170_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"S0956796819000170_ref91","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976013"},{"key":"S0956796819000170_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_7"},{"key":"S0956796819000170_ref95","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"S0956796819000170_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"S0956796819000170_ref53","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599422"},{"key":"S0956796819000170_ref55","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000093"},{"key":"S0956796819000170_ref56","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428121"},{"key":"S0956796819000170_ref70","unstructured":"Jacob-Rao, R. , Pientka, B. & Thibodeau, D. (2018) Index-stratified types. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK , Kirchner, H. (ed). LIPIcs, vol. 108. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 19:1\u201319:17."},{"key":"S0956796819000170_ref60","unstructured":"Girard, J. Y. (1972) Interpr\u00e9tation fonctionnelle et elimination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. These d\u2019\u00e9tat, Universit\u00e9 de Paris 7."},{"key":"S0956796819000170_ref62","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014053"},{"key":"S0956796819000170_ref66","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"S0956796819000170_ref101","unstructured":"Poulsen, C. B. , Rouvoet, A. , Tolmach, A. , Krebbers, R. & Visser, E. (2018). Intrinsically-typed definitional interpreters for imperative languages. PACMPL 2(POPL), 16:1\u201316:34."},{"key":"S0956796819000170_ref69","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"S0956796819000170_ref73","doi-asserted-by":"crossref","unstructured":"Keuchel, S. , Weirich, S. & Schrijvers, T. (2016) Needle & Knot: Binder boilerplate tied up. In European Symposium on Programming. Springer, pp. 419\u2013445.","DOI":"10.1007\/978-3-662-49498-1_17"},{"key":"S0956796819000170_ref80","doi-asserted-by":"publisher","DOI":"10.1145\/1631687.1596571"},{"key":"S0956796819000170_ref63","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_26"},{"key":"S0956796819000170_ref74","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"S0956796819000170_ref75","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"S0956796819000170_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018613"},{"key":"S0956796819000170_ref77","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_22"},{"key":"S0956796819000170_ref81","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09527-x"},{"key":"S0956796819000170_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863547"},{"key":"S0956796819000170_ref58","unstructured":"Gacek, A. (2010) Girard\u2019s Proof of Strong Normalization of the Simply-Typed Lambda-Calculus Calculus. http:\/\/abella-prover.org\/examples\/lambda-calculus\/normalization\/stlc-strong-norm.html."},{"key":"S0956796819000170_ref78","doi-asserted-by":"publisher","DOI":"10.1145\/3167083"},{"key":"S0956796819000170_ref79","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"S0956796819000170_ref84","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90067-V"},{"key":"S0956796819000170_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"S0956796819000170_ref87","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"S0956796819000170_ref102","doi-asserted-by":"publisher","DOI":"10.1145\/2503887.2503891"},{"key":"S0956796819000170_ref88","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.09.014"},{"key":"S0956796819000170_ref57","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0064870"},{"key":"S0956796819000170_ref90","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.08.001"},{"key":"S0956796819000170_ref31","first-page":"50","article-title":"Extracting a normalization algorithm in Isabelle\/HOL. In TYPES. Lecture Notes in","volume":"3839","author":"Berghofer","year":"2004","journal-title":"Computer Science"},{"key":"S0956796819000170_ref92","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-6534-3"},{"key":"S0956796819000170_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_11"},{"key":"S0956796819000170_ref94","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"S0956796819000170_ref93","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_19"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796819000170","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,10]],"date-time":"2019-12-10T02:52:08Z","timestamp":1575946328000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796819000170\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"references-count":118,"alternative-id":["S0956796819000170"],"URL":"https:\/\/doi.org\/10.1017\/s0956796819000170","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"article-number":"e19"}}