{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T04:45:58Z","timestamp":1760244358321,"version":"build-2065373602"},"reference-count":29,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T00:00:00Z","timestamp":1672358400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Axioms"],"abstract":"<jats:p>In this paper, we develop, in the proof assistant Coq, a definitional interpreter and a type-checker for a simply typed functional language, and formally prove that the mentioned type-checker is sound with respect to the definitional interpreter via progress and preservation. To represent binders, we embark on the choice of \u201cconcrete syntax\u201d in which parameters are just names (or strings).<\/jats:p>","DOI":"10.3390\/axioms12010043","type":"journal-article","created":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T03:08:59Z","timestamp":1672628939000},"page":"43","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Sound Definitional Interpreter for a Simply Typed Functional Language"],"prefix":"10.3390","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6602-7906","authenticated-orcid":false,"given":"Burak","family":"Ekici","sequence":"first","affiliation":[{"name":"Department of Computer Engineering, Mu\u011fla S\u0131tk\u0131 Ko\u00e7man University, Mu\u011fla 48000, Turkey"}]}],"member":"1968","published-online":{"date-parts":[[2022,12,30]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1023\/A:1010027404223","article-title":"Definitional Interpreters for Higher-Order Programming Languages","volume":"11","author":"Reynolds","year":"1998","journal-title":"High. Order Symb. Comput."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A Formulation of the Simple Theory of Types","volume":"5","author":"Church","year":"1940","journal-title":"J. Symb. Log."},{"key":"ref_3","unstructured":"The Coq Development Team (2018). The Coq Proof Assistant Reference Manual, The Coq Development Team."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","article-title":"A Syntactic Approach to Type Soundness","volume":"115","author":"Wright","year":"1994","journal-title":"Inf. Comput."},{"key":"ref_5","first-page":"16:1","article-title":"Intrinsically-typed definitional interpreters for imperative languages","volume":"2","author":"Poulsen","year":"2018","journal-title":"Proc. ACM Program. Lang."},{"key":"ref_6","first-page":"453","article-title":"Monadic Presentations of Lambda Terms Using Generalized Inductive Types","volume":"Volume 1683","author":"Flum","year":"1999","journal-title":"Proceedings of the Computer Science Logic, 13th International Workshop, CSL \u201999, 8th Annual Conference of the EACSL"},{"key":"ref_7","first-page":"1","article-title":"The Meaning of Types From Intrinsic to Extrinsic Semantics","volume":"7","author":"Reynolds","year":"2000","journal-title":"BRICS Rep. Ser."},{"key":"ref_8","unstructured":"Augustsson, L., and Carlsson, M. (2022, September 04). An exercise in dependent types: A well-typed interpreter. In Workshop on Dependent Types in Programming, Gothenburg; 1999. Available online: https:\/\/www.semanticscholar.org\/paper\/An-exercise-in-dependent-types%3A-A-well-typed-Augustsson-Carlsson\/5dae20b002f4e9d91e60db6af192c69d7fe764c6."},{"key":"ref_9","unstructured":"Blanchette, J., and Hritcu, C. (2020, January 20\u201321). Intrinsically-typed definitional interpreters for linear, session-typed languages. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"12:1","DOI":"10.1145\/3110256","article-title":"Abstracting definitional interpreters (functional pearl)","volume":"1","author":"Darais","year":"2017","journal-title":"Proc. ACM Program. Lang."},{"key":"ref_11","unstructured":"Aldrich, J., and Eugster, P. (2015, January 25\u201330). Galois transformers and modular abstract interpreters: Reusable metatheory for program analysis. Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA."},{"key":"ref_12","unstructured":"Boehm, H., and Flanagan, C. (2013, January 16\u201319). Monadic abstract interpreters. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, Seattle, WA, USA."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1017\/S0956796814000100","article-title":"Pushdown flow analysis with abstract garbage collection","volume":"24","author":"Johnson","year":"2014","journal-title":"J. Funct. Program."},{"key":"ref_14","first-page":"250","article-title":"Simulation of Two-Way Pushdown Automata Revisited","volume":"Volume 129","author":"Banerjee","year":"2013","journal-title":"Proceedings of the Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, EPTCS"},{"key":"ref_15","unstructured":"Black, A.P., and Tratt, L. (2014, January 20\u201324). Abstracting abstract control. Proceedings of the DLS\u201914, Proceedings of the 10th ACM Symposium on Dynamic Languages, part of SLASH 2014, Portland, OR, USA."},{"key":"ref_16","unstructured":"Bod\u00edk, R., and Majumdar, R. (2016, January 20\u201322). Pushdown control-flow analysis for free. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA."},{"key":"ref_17","unstructured":"Castagna, G., and Gordon, A.D. (2017, January 18\u201320). Type soundness proofs with definitional interpreters. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France."},{"key":"ref_18","unstructured":"Pierce, B.C., de Amorim, A.A., Casinghino, C., Gaboardi, M., Greenberg, M., Hri\u0163cu, C., Sj\u00f6berg, V., Tolmach, A., and Yorgey, B. (2022). Programming Language Foundations, Electronic textbook. Available online: http:\/\/www.cis.upenn.edu\/~bcpierce\/sf."},{"key":"ref_19","unstructured":"Koprowski, A. (2006). A Formalization of the Simply Typed Lambda Calculus in Coq, INRIA."},{"key":"ref_20","unstructured":"Wei, G. (2018, August 01). A Soundness Proof of STLC by Definitional Interpreters in Agda. Available online: https:\/\/continuation.passing.style\/blog\/stlc-soundness.html."},{"key":"ref_21","unstructured":"van Der Bilt, P., and STLC in Coq Extended with a Sound Big-Step Semantics, Functions as Closures and Records as Lists (2019, August 01). Coq-Lang-Playarea. Available online: https:\/\/github.com\/pvanderbilt\/coq-lang-playarea."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","article-title":"Introduction to Generalized Type Systems","volume":"1","author":"Barendregt","year":"1991","journal-title":"J. Funct. Program."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","article-title":"The System F of Variable Types, Fifteen Years Later","volume":"45","author":"Girard","year":"1986","journal-title":"Theor. Comput. Sci."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The Calculus of Constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inf. Comput."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","article-title":"Notions of Computation and Monads","volume":"93","author":"Moggi","year":"1991","journal-title":"Inf. Comput."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Nicolaas Govert de Bruijn (1972). Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math. Proc., 75, 381\u2013392.","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","article-title":"The Locally Nameless Representation","volume":"49","year":"2012","journal-title":"J. Autom. Reason."},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Chlipala, A. (2008, January 20\u201328). Parametric higher-order abstract syntax for mechanized semantics. Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, Victoria, BC, Canada.","DOI":"10.1145\/1411204.1411226"},{"key":"ref_29","first-page":"29:1","article-title":"Reaching for the Star: Tale of a Monad in Coq","volume":"Volume 193","author":"Cohen","year":"2021","journal-title":"Proceedings of the 12th International Conference on Interactive Theorem Proving, ITP 2021"}],"container-title":["Axioms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2075-1680\/12\/1\/43\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T01:48:40Z","timestamp":1760147320000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2075-1680\/12\/1\/43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,30]]},"references-count":29,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,1]]}},"alternative-id":["axioms12010043"],"URL":"https:\/\/doi.org\/10.3390\/axioms12010043","relation":{},"ISSN":["2075-1680"],"issn-type":[{"type":"electronic","value":"2075-1680"}],"subject":[],"published":{"date-parts":[[2022,12,30]]}}}