Casper Bach Poulsen
Arjen Rouvoet
Eelco Visser
Skip Abstract Section
Skip Supplemental Material SectionAbstract
A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a separate type system requires a separate type safety proof. An alternative approach, at least for pure object languages, is to use a dependently-typed language to encode the object language type system in the definition of the abstract syntax. Using such intrinsically-typed abstract syntax definitions allows the host language type checker to verify automatically that the interpreter satisfies type safety. Does this approach scale to larger and more realistic object languages, and in particular to languages with mutable state and objects?
In this paper, we describe and demonstrate techniques and libraries in Agda that successfully scale up intrinsically-typed definitional interpreters to handle rich object languages with non-trivial binding structures and mutable state. While the resulting interpreters are certainly more complex than the simply-typed λ-calculus interpreter we start with, we claim that they still meet the goals of being concise, comprehensible, and executable, while guaranteeing type safety for more elaborate object languages. We make the following contributions: (1) A dependent-passing style technique for hiding the weakening of indexed values as they propagate through monadic code. (2) An Agda library for programming with scope graphs and frames, which provides a uniform approach to dealing with name binding in intrinsically-typed interpreters. (3) Case studies of intrinsically-typed definitional interpreters for the simply-typed λ-calculus with references (STLC+Ref) and for a large subset of Middleweight Java (MJ).
Supplemental Material
Available for Download
zip
popl18-p277-aux.zip (1.2 MB)
This artifact describes and demonstrates techniques and libraries in Agda that successfully scale up intrinsically-typed definitional interpreters to handle rich object languages with non-trivial binding structures and mutable state.
- Reynald Affeldt and Kazuhiko Sakaguchi. 2014. An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing. Journal of Formalized Reasoning 7, 1 (2014), 63–104. Google Scholar
Digital Library
- Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. 2018. Recalling a Witness. In Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2018, Los Angeles, CA, USA, January 8-13, 2018 . ACM.Google Scholar
- Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. 2017. Dijkstra Monads for Free. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017) . ACM, New York, NY, USA, 515–529. Google ScholarDigital Library
- Guillaume Allais, James Chapman, Conor McBride, and James McKinna. 2017. Type-and-scope safe programs and their proofs. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017 , Yves Bertot and Viktor Vafeiadis (Eds.). ACM, 195–207. Google ScholarDigital Library
- Thorsten Altenkirch and Ambrus Kaposi. 2016a. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal (LIPIcs) , Delia Kesner and Brigitte Pientka (Eds.), Vol. 52. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. Google ScholarCross Ref
- Thorsten Altenkirch and Ambrus Kaposi. 2016b. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 , Rastislav Bodik and Rupak Majumdar (Eds.). ACM, 18–29. Google ScholarDigital Library
- Thorsten Altenkirch and Bernhard Reus. 1999. Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In Computer Science Logic, 13th International Workshop, CSL 99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings (Lecture Notes in Computer Science) , Jörg Flum and Mario Rodríguez-Artalejo (Eds.), Vol. 1683. Springer, 453–468. Google ScholarCross Ref
- Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 666–679. Google ScholarDigital Library
- Robert Atkey. 2009. Parameterised notions of computation. Journal of Functional Programming 19, 3-4 (2009), 335–376. Google ScholarDigital Library
- Lennart Augustsson and Magnus Carlsson. 1999. An exercise in dependent types: A well-typed interpreter. In In Workshop on Dependent Types in Programming, Gothenburg .Google Scholar
- Casper Bach Poulsen, Pierre Néron, Andrew P. Tolmach, and Eelco Visser. 2016. Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics. In 30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy (LIPIcs) , Shriram Krishnamurthi and Benjamin S. Lerner (Eds.), Vol. 56. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik. Google ScholarCross Ref
- Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. 2017. Artifact Intrinsically-Typed Definitional Interpreters for Imperative Languages. https://github.com/metaborg/mj.agdaGoogle Scholar
- David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and YuTing Wang. 2014. Abella: A System for Reasoning about Relational Specifications. J. Formalized Reasoning 7, 2 (2014), 1–89. Google ScholarCross Ref
- Nick Benton, Chung-Kil Hur, Andrew Kennedy, and Conor McBride. 2012. Strongly Typed Term Representations in Coq. Journal of Automated Reasoning 49, 2 (2012), 141–159. Google ScholarDigital Library
- Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions . Springer. Google ScholarCross Ref
- G. M. Bierman, M. J. Parkinson, and A. M. Pitts. 2003. MJ: An imperative core calculus for Java and Java with effects. Technical Report UCAM-CL-TR-563. University of Cambridge.Google Scholar
- Richard S. Bird and Lambert G. L. T. Meertens. 1998. Nested Datatypes. In Mathematics of Program Construction, MPC 98, Marstrand, Sweden, June 15-17, 1998, Proceedings (Lecture Notes in Computer Science) , Johan Jeuring (Ed.), Vol. 1422. Springer, 52–67. Google ScholarCross Ref
- Denis Bogdanas and Grigore Rosu. 2015. K-Java: A Complete Semantics of Java. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015 , Sriram K. Rajamani and David Walker (Eds.). ACM, 445–456. Google ScholarDigital Library
- Edwin Brady. 2013a. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593. Google ScholarCross Ref
- Edwin Brady. 2013b. Programming and reasoning with algebraic effects and dependent types. In ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013 , Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 133–144. Google ScholarDigital Library
- Edwin Brady and Kevin Hammond. 2006. A verified staged interpreter is a verified compiler. In Generative Programming and Component Engineering, 5th International Conference, GPCE 2006, Portland, Oregon, USA, October 22-26, 2006, Proceedings , Stan Jarzabek, Douglas C. Schmidt, and Todd L. Veldhuizen (Eds.). ACM, 111–120. Google ScholarDigital Library
- Venanzio Capretta. 2005. General recursion via coinductive types. Logical Methods in Computer Science 1, 2 (2005). Google ScholarCross Ref
- James Chapman. 2009. Type Theory Should Eat Itself. Electronic Notes in Theoretical Computer Science 228 (2009), 21–36. Google ScholarDigital Library
- Adam Chlipala. 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press.Google ScholarDigital Library
- Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. 2009. Effective Interactive Proofs for Higher-order Imperative Programs. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP ’09) . ACM, New York, NY, USA, 79–90. Google ScholarDigital Library
- Matteo Cimini, Dale Miller, and Jeremy G. Siek. 2016. Well-Typed Languages are Sound. CoRR abs/1611.05105 (2016). http://arxiv.org/abs/1611.05105Google Scholar
- Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott (Eds.). 2007. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic . Lecture Notes in Computer Science, Vol. 4350. Springer.Google Scholar
- The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual. http://coq.inria.fr/doc/Google Scholar
- Nils Anders Danielsson. 2012. Operational semantics using the partiality monad. In ACM SIGPLAN International Conference on Functional Programming, ICFP’12, Copenhagen, Denmark, September 9-15, 2012 , Peter Thiemann and Robby Bruce Findler (Eds.). ACM, 127–138. Google ScholarDigital Library
- Nils Anders Danielsson and U Norell. 2017. The Agda standard library. https://github.com/agda/agda-stdlibGoogle Scholar
- N. G. de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, 5 (1972), 381–392. Google ScholarCross Ref
- Benjamin Delaware, William R. Cook, and Don S. Batory. 2011. Product lines of theorems. In Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, October 22 - 27, 2011 , Cristina Videira Lopes and Kathleen Fisher (Eds.). ACM, 595–608. Google ScholarDigital Library
- Dominique Devriese and Frank Piessens. 2011. On the bright side of type classes: instance arguments in Agda. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011 , Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy (Eds.). ACM, 143–155. Google ScholarDigital Library
- Sylvia Grewe, Sebastian Erdweg, Pascal Wittmann, and Mira Mezini. 2015. Type systems for the masses: deriving soundness proofs and efficient checkers. In 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2015, Pittsburgh, PA, USA, October 25-30, 2015 , Gail C. Murphy and Guy L. Steele Jr. (Eds.). ACM, 137–150. Google ScholarDigital Library
- Peter Hancock and Anton Setzer. 2000. Interactive Programs in Dependent Type Theory. In Computer Science Logic, 14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings (Lecture Notes in Computer Science) , Peter Clote and Helmut Schwichtenberg (Eds.), Vol. 1862. Springer, 317–331. Google ScholarCross Ref
- Robert Harper. 1994. A Simplified Account of Polymorphic References. Inf. Process. Lett. 51, 4 (1994), 201–206. Google ScholarDigital Library
- Robert Harper and Christopher A. Stone. 2000. A type-theoretic interpretation of standard ML. In Proof, Language, and Interaction, Essays in Honour of Robin Milner , Gordon D. Plotkin, Colin Stirling, and Mads Tofte (Eds.). The MIT Press, 341–388.Google Scholar
- Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 2001. Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems 23, 3 (2001), 396–450. Google ScholarDigital Library
- Lennart C. L. Kats and Eelco Visser. 2010. The Spoofax language workbench: rules for declarative specification of languages and IDEs. In Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010 , William R. Cook, Siobhán Clarke, and Martin C. Rinard (Eds.). ACM, Reno/Tahoe, Nevada, 444–463. Google ScholarDigital Library
- Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. 2012. Run your research: on the effectiveness of lightweight mechanization. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012 , John Field and Michael Hicks (Eds.). ACM, 285–296. Google ScholarDigital Library
- Gerwin Klein and Tobias Nipkow. 2005. Jinja is not Java. Archive of Formal Proofs 2005 (2005).Google Scholar
- Gerwin Klein and Tobias Nipkow. 2006. A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Transactions on Programming Languages and Systems 28, 4 (2006), 619–695. Google ScholarDigital Library
- Anders Kock. 1972. Strong functors and monoidal monads. Archiv der Mathematik 23, 1 (Dec 1972), 113–120. Google ScholarCross Ref
- Gabriël D. P. Konat, Lennart C. L. Kats, Guido Wachsmuth, and Eelco Visser. 2012. Declarative Name Binding and Scope Rules. In Software Language Engineering, 5th International Conference, SLE 2012, Dresden, Germany, September 26-28, 2012, Revised Selected Papers (Lecture Notes in Computer Science) , Krzysztof Czarnecki and Görel Hedin (Eds.), Vol. 7745. Springer, 311–331. Google ScholarCross Ref
- Joomy Korkut, Maksim Trifunovski, and Daniel R. Licata. 2016. Intrinsic Verification of a Regular Expression Matcher. (2016). http://dlicata.web.wesleyan.edu/pubs/ktl16regexp/ktl16regexp.pdf Unpublished draft.Google Scholar
- Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 205–217. Google ScholarDigital Library
- Daniel R. Licata and Robert Harper. 2009. Positively dependent types. In Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009 , Thorsten Altenkirch and Todd D. Millstein (Eds.). ACM, 3–14. Google ScholarDigital Library
- Florian Lorenzen and Sebastian Erdweg. 2016. Sound type-dependent syntactic language extension. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 , Rastislav Bodik and Rupak Majumdar (Eds.). ACM, 204–216. Google ScholarDigital Library
- Julian Mackay, Hannes Mehnert, Alex Potanin, Lindsay Groves, and Nicholas R. Cameron. 2012. Encoding Featherweight Java with assignment and immutability using the Coq proof assistant. In Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, FTfJP 2012, Beijing, China, June 12, 2012 , Wei-Ngan Chin and Aquinas Hobor (Eds.). ACM, 11–19. Google ScholarDigital Library
- Conor McBride. 2010. Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In Proceedings of the ACM SIGPLAN Workshop on Generic Programming, WGP 2010, Baltimore, MD, USA, September 27-29, 2010 , Bruno C. d. S. Oliveira and Marcin Zalewski (Eds.). ACM, 1–12. Google ScholarDigital Library
- Conor McBride. 2011. Kleisli Arrows of Outrageous Fortune. (2011). Accepted for publication.Google Scholar
- Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. 1997. The Definition of Standard ML, Revised. MIT Press, Cambridge, MA, USA.Google Scholar
- Eugenio Moggi. 1991. Notions of Computation and Monads. Inf. Comput. 93, 1 (July 1991), 55–92. Google ScholarDigital Library
- Peter D. Mosses. 1999. A Modular SOS for ML Concurrency Primitives. BRICS Research Series RS-99-57. Department of Computer Science, Aarhus University.Google Scholar
- Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. 2014. Lem: reusable engineering of real-world semantics. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014 , Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 175–188. Google ScholarDigital Library
- Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. 2008. Hoare Type Theory, Polymorphism and Separation1. J. Funct. Program. 18, 5-6 (Sept. 2008), 865–911. Google ScholarDigital Library
- Tobias Nipkow and Gerwin Klein. 2014. Concrete Semantics - With Isabelle/HOL. Springer. Google ScholarCross Ref
- Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden.Google Scholar
- Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. 2015. A Theory of Name Resolution. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings (Lecture Notes in Computer Science) , Jan Vitek (Ed.), Vol. 9032. Springer, 205–231. Google ScholarCross Ref
- Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (Lecture Notes in Computer Science) , Vol. 9632. Springer Berlin Heidelberg, Berlin, Heidelberg, 589–615. Google ScholarDigital Library
- Frank Pfenning and Conal Elliott. 1988. Higher-Order Abstract Syntax. In PLDI. 199–208. Google ScholarDigital Library
- Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, Massachusetts.Google ScholarDigital Library
- The Racket Development Team. 2017. Racket v6.11. http://blog.racket-lang.org/2017/10/racket-v6-11.htmlGoogle Scholar
- John Reynolds. 2004. The Meaning of Types – From Intrinsic to Extrinsic Semantics. BRICS Research Series RS-00-32. Department of Computer Science, Aarhus University.Google Scholar
- John C. Reynolds. 1972. Definitional Interpreters for Higher-order Programming Languages. In Proceedings of the ACM Annual Conference - Volume 2 (ACM ’72) . ACM, New York, NY, USA, 717–740. Google ScholarDigital Library
- Grigore Rosu and Traian-Florin Serbanuta. 2010. An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79, 6 (2010), 397–434. Google ScholarCross Ref
- Jeremy G. Siek. 2013. Type Safety in Three Easy Lemmas. http://siek.blogspot.co.uk/2013/05/ type-safety-in-three-easy-lemmas.html .Google Scholar
- Matthieu Sozeau. 2008. Un environnement pour la programmation avec types dépendants. (An environment for programming with dependent types) . Ph.D. Dissertation. University of Paris-Sud, Orsay, France.Google Scholar
- Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Rosu. 2016. Semantics-based program verifiers for all languages. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016 , Eelco Visser and Yannis Smaragdakis (Eds.). ACM, 74–91. Google ScholarDigital Library
- Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. 2013. Verifying higher-order programs with the dijkstra monad. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013 , Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 387–398. Google ScholarDigital Library
- S. Doaitse Swierstra, Marcos Viera, and Atze Dijkstra. 2016. A Lazy Language Needs a Lazy Type System: Introducing Polymorphic Contexts. In Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages, IFL 2016, Leuven, Belgium, August 31 - September 2, 2016 , Tom Schrijvers (Ed.). ACM. Google ScholarDigital Library
- Wouter Swierstra. 2009a. A functional specification of effects. Ph.D. Dissertation. University of Nottingham, UK.Google Scholar
- Wouter Swierstra. 2009b. A Hoare Logic for the State Monad. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings (Lecture Notes in Computer Science) , Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674. Springer, 440–451. Google ScholarDigital Library
- Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. 2016. A constraint language for static semantic analysis based on scope graphs. In Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 , Martin Erwig and Tiark Rompf (Eds.). ACM, 49–60. Google ScholarDigital Library
- L. Thomas van Binsbergen, Neil Sculthorpe, and Peter D. Mosses. 2016. Tool support for component-based semantics. In Companion Proceedings of the 15th International Conference on Modularity, Málaga, Spain, March 14 - 18, 2016, Lidia Fuentes, Don S. Batory, and Krzysztof Czarnecki (Eds.). ACM, 8–11. Google ScholarDigital Library
- Vlad A. Vergu, Pierre Néron, and Eelco Visser. 2015. DynSem: A DSL for Dynamic Semantics Specification. In 26th International Conference on Rewriting Techniques and Applications, RTA 2015, June 29 to July 1, 2015, Warsaw, Poland (LIPIcs) , Maribel Fernández (Ed.), Vol. 36. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 365–378. Google ScholarCross Ref
- Eelco Visser, Guido Wachsmuth, Andrew P. Tolmach, Pierre Néron, Vlad A. Vergu, Augusto Passalaqua, and Gabriël D. P. Konat. 2014. A Language Designer’s Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs. In Onward! 2014, Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, part of SPLASH ’14, Portland, OR, USA, October 20-24, 2014 , Andrew P. Black, Shriram Krishnamurthi, Bernd Bruegge, and Joseph N. Ruskiewicz (Eds.). ACM, 95–111. Google ScholarDigital Library
- Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115, 1 (November 1994), 38–94. Google ScholarDigital Library
- Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded recursive datatype constructors. In POPL. 224–235. Google ScholarDigital Library
Index Terms
- Intrinsically-typed definitional interpreters for imperative languages
Recommendations
Intrinsically-typed definitional interpreters à la carte
Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular ...
Intrinsically typed compilation with nameless labels
To avoid compilation errors it is desirable to verify that a compiler is type correct—i.e., given well-typed source code, it always outputs well-typed target code. This can be done intrinsically by implementing it as a function in a dependently typed ...
Intrinsically-typed definitional interpreters for linear, session-typed languages
CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and ProofsAn intrinsically-typed definitional interpreter is a concise specification of dynamic semantics, that is executable and type safe by construction. Unfortunately, scaling intrinsically-typed definitional interpreters to more complicated object languages ...
Comments