publications:
- title: "A verified information-flow architecture"
  author:
  - name: "Arthur Azevedo de Amorim"
    link: "https://researchr.org/alias/arthur-azevedo-de-amorim"
  - name: "Nathan Collins"
    link: "https://researchr.org/alias/nathan-collins"
  - name: "André DeHon"
    link: "https://researchr.org/alias/andr%C3%A9-dehon"
  - name: "Delphine Demange"
    link: "https://researchr.org/alias/delphine-demange"
  - name: "Catalin Hritcu"
    link: "https://researchr.org/alias/catalin-hritcu"
  - name: "David Pichardie"
    link: "https://researchr.org/alias/david-pichardie"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "Randy Pollack"
    link: "https://researchr.org/alias/randy-pollack"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2535838.2535839"
  links:
    doi: "http://doi.acm.org/10.1145/2535838.2535839"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/AmorimCDDHPPPT14"
  researchr: "https://researchr.org/publication/AmorimCDDHPPPT14"
  cites: 0
  citedby: 0
  pages: "165-178"
  booktitle: "The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014"
  editor:
  - name: "Suresh Jagannathan"
    link: "https://researchr.org/alias/suresh-jagannathan"
  - name: "Peter Sewell"
    link: "https://researchr.org/alias/peter-sewell"
  publisher: "ACM"
  isbn: "978-1-4503-2544-8"
  kind: "inproceedings"
  key: "AmorimCDDHPPPT14"
- title: "A constraint language for static semantic analysis based on scope graphs"
  author:
  - name: "Hendrik van Antwerpen"
    link: "https://nl.linkedin.com/in/hendrikvanantwerpen"
  - name: "Pierre Néron"
    link: "https://researchr.org/profile/pierrejeanmichelneron/publications"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  - name: "Guido Wachsmuth"
    link: "https://www.linkedin.com/in/guidowachsmuth/"
  year: "2016"
  doi: "http://doi.acm.org/10.1145/2847538.2847543"
  abstract: "In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs -- such as record field access -- for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records. "
  links:
    doi: "http://doi.acm.org/10.1145/2847538.2847543"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pepm/AntwerpenNTVW16"
  researchr: "https://researchr.org/publication/AntwerpenNTVW16"
  cites: 0
  citedby: 0
  pages: "49-60"
  booktitle: "Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016"
  editor:
  - name: "Martin Erwig"
    link: "https://researchr.org/alias/martin-erwig"
  - name: "Tiark Rompf"
    link: "https://researchr.org/alias/tiark-rompf"
  publisher: "ACM"
  isbn: "978-1-4503-4097-7"
  kind: "inproceedings"
  key: "AntwerpenNTVW16"
- title: "Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics"
  author:
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Pierre Néron"
    link: "https://researchr.org/profile/pierrejeanmichelneron/publications"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2016"
  doi: "10.4230/LIPIcs.ECOOP.2016.20"
  abstract: "Semantic specifications do not make a systematic connection between the names and scopes in the static structure of a program and memory layout, and access during its execution. In this paper, we introduce a systematic approach to the alignment of names in static semantics and memory in dynamic semantics, building on the scope graph framework for name resolution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection. "
  links:
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ecoop/PoulsenNTV16"
    technicalreport: "https://researchr.org/publication/TUD-SERG-2016-010"
    "pdf": "http://drops.dagstuhl.de/opus/volltexte/2016/6114/pdf/LIPIcs-ECOOP-2016-20.pdf"
  researchr: "https://researchr.org/publication/PoulsenNTV16"
  cites: 0
  citedby: 0
  booktitle: "30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy"
  editor:
  - name: "Shriram Krishnamurthi"
    link: "https://researchr.org/alias/shriram-krishnamurthi"
  - name: "Benjamin S. Lerner"
    link: "https://researchr.org/alias/benjamin-s.-lerner"
  volume: "56"
  series: "LIPIcs"
  publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik"
  isbn: "978-3-95977-014-9"
  kind: "inproceedings"
  key: "PoulsenNTV16"
- title: "Lightweight concurrency primitives for GHC"
  author:
  - name: "Peng Li"
    link: "https://researchr.org/alias/peng-li"
  - name: "Simon Marlow"
    link: "https://researchr.org/alias/simon-marlow"
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1291201.1291217"
  links:
    doi: "http://doi.acm.org/10.1145/1291201.1291217"
  tags:
  - "Haskell"
  researchr: "https://researchr.org/publication/LiMJT07"
  cites: 0
  citedby: 0
  pages: "107-118"
  booktitle: "Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2007, Freiburg, Germany, September 30, 2007"
  editor:
  - name: "Gabriele Keller"
    link: "https://researchr.org/alias/gabriele-keller"
  publisher: "ACM"
  isbn: "978-1-59593-674-5"
  kind: "inproceedings"
  key: "LiMJT07"
- title: "From ML to Ada: Strongly-Typed Language Interoperability via Source Translation"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Dino Oliva"
    link: "https://researchr.org/alias/dino-oliva"
  year: "1998"
  tags:
  - "translation"
  - "source-to-source"
  - "open-source"
  researchr: "https://researchr.org/publication/TolmachO98"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "8"
  number: "4"
  pages: "367-412"
  kind: "article"
  key: "TolmachO98"
- title: "Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics"
  author:
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Pierre Neron"
    link: "http://www.lix.polytechnique.fr/~neron/"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2016"
  links:
    published: "https://researchr.org/publication/PoulsenNTV16"
    "pdf": "http://swerl.tudelft.nl/twiki/pub/Main/TechnicalReports/TUD-SERG-2016-010.pdf"
  researchr: "https://researchr.org/publication/TUD-SERG-2016-010"
  cites: 0
  citedby: 0
  institution: "Delft University of Technology, Programming Languages Research Group"
  number: "TUD-SERG-2016-010"
  address: "Delft, The Netherlands"
  kind: "techreport"
  key: "TUD-SERG-2016-010"
- title: "A Constraint Language for Static Semantic Analysis based on Scope Graphs with Proofs"
  author:
  - name: "Hendrik van Antwerpen"
    link: "https://nl.linkedin.com/in/hendrikvanantwerpen"
  - name: "Pierre Néron"
    link: "https://researchr.org/profile/pierrejeanmichelneron/publications"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  - name: "Guido Wachsmuth"
    link: "https://www.linkedin.com/in/guidowachsmuth/"
  year: "2015"
  month: "November"
  abstract: "In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs -- such as record field access -- for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records."
  note: "Available at \\url{http://swerl.tudelft.nl/twiki/pub/Main/TechnicalReports/TUD-SERG-2015-012.pdf}"
  links:
    published: "https://researchr.org/publication/VanAntwerpenNTVWPEPM2016"
  researchr: "https://researchr.org/publication/TUD-SERG-2015-012"
  cites: 0
  citedby: 0
  institution: "Software Engineering Research Group, Delft University of Technology"
  number: "TUD-SERG-2015-012"
  kind: "techreport"
  key: "TUD-SERG-2015-012"
- title: "Debuggable Concurrency Extensions for Standard ML"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1991"
  tags:
  - "debugging"
  researchr: "https://researchr.org/publication/TolmachA91"
  cites: 0
  citedby: 0
  pages: "120-131"
  booktitle: "Workshop on Parallel and Distributed Debugging"
  kind: "inproceedings"
  key: "TolmachA91"
- title: "A principled approach to operating system construction in Haskell"
  author:
  - name: "Thomas Hallgren"
    link: "https://researchr.org/alias/thomas-hallgren"
  - name: "Mark P. Jones"
    link: "https://researchr.org/alias/mark-p.-jones"
  - name: "Rebekah Leslie"
    link: "https://researchr.org/alias/rebekah-leslie"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1086365.1086380"
  abstract: " We describe a monadic interface to low-level hardware features that is a suitable basis for building operating systems in Haskell. The interface includes primitives for controlling memory management hardware, user-mode process execution, and low-level device I/O. The interface enforces memory safety in nearly all circumstances. Its behavior is specified in part by formal assertions written in a programming logic called P-Logic. The interface has been implemented on bare IA32 hardware using the Glasgow Haskell Compiler (GHC) runtime system. We show how a variety of simple O/S kernels can be constructed on top of the interface, including a simple separation kernel and a demonstration system in which the kernel, window system, and all device drivers are written in Haskell. "
  links:
    doi: "http://doi.acm.org/10.1145/1086365.1086380"
  tags:
  - "control systems"
  - "operating system"
  - "memory management"
  - "Haskell"
  - "logic programming"
  - "compiler"
  - "programming"
  - "logic"
  - "systematic-approach"
  researchr: "https://researchr.org/publication/HallgrenJLT05"
  cites: 0
  citedby: 0
  pages: "116-128"
  booktitle: "Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005"
  editor:
  - name: "Olivier Danvy"
    link: "https://www.yale-nus.edu.sg/about/faculty/olivier-danvy/"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  publisher: "ACM"
  isbn: "1-59593-064-7"
  kind: "inproceedings"
  key: "HallgrenJLT05"
- title: "Implementing functional logic languages using multiple threads and stores"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Sergio Antoy"
    link: "http://web.cecs.pdx.edu/~antoy/"
  - name: "Marius Nita"
    link: "https://researchr.org/alias/marius-nita"
  year: "2004"
  doi: "http://doi.acm.org/10.1145/1016850.1016865"
  links:
    doi: "http://doi.acm.org/10.1145/1016850.1016865"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/TolmachAN04"
  cites: 0
  citedby: 0
  pages: "90-102"
  booktitle: "Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird, UT, USA, September 19-21, 2004"
  editor:
  - name: "Chris Okasaki"
    link: "https://researchr.org/alias/chris-okasaki"
  - name: "Kathleen Fisher"
    link: "http://www.research.att.com/people/Fisher_Kathleen_S"
  publisher: "ACM"
  isbn: "1-58113-905-5"
  kind: "inproceedings"
  key: "TolmachAN04"
- title: "A Virtual Machine for Functional Logic Computations"
  author:
  - name: "Sergio Antoy"
    link: "http://web.cecs.pdx.edu/~antoy/"
  - name: "Michael Hanus"
    link: "http://www.informatik.uni-kiel.de/~mh/"
  - name: "Jimeng Liu"
    link: "https://researchr.org/alias/jimeng-liu"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2004"
  doi: "http://dx.doi.org/10.1007/11431664_7"
  links:
    doi: "http://dx.doi.org/10.1007/11431664_7"
  tags:
  - "logic"
  researchr: "https://researchr.org/publication/AntoyHLT04"
  cites: 0
  citedby: 0
  pages: "108-125"
  booktitle: "Implementation and Application of Functional Languages, 16th International Workshop, IFL 2004, Lübeck, Germany, September 8-10, 2004, Revised Selected Papers"
  editor:
  - name: "Clemens Grelck"
    link: "https://researchr.org/alias/clemens-grelck"
  - name: "Frank Huch"
    link: "https://researchr.org/alias/frank-huch"
  - name: "Greg Michaelson"
    link: "https://researchr.org/alias/greg-michaelson"
  - name: "Philip W. Trinder"
    link: "https://researchr.org/alias/philip-w.-trinder"
  volume: "3474"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-26094-3"
  kind: "inproceedings"
  key: "AntoyHLT04"
- title: "Typed Higher-Order Narrowing without Higher-Order Strategies"
  author:
  - name: "Sergio Antoy"
    link: "http://web.cecs.pdx.edu/~antoy/"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "1999"
  researchr: "https://researchr.org/publication/AntoyT99"
  cites: 0
  citedby: 0
  pages: "335-353"
  booktitle: "Functional and Logic Programming, 4th Fuji International Symposium, FLOPS 99, Tsukuba, Japan, November 11-13, 1999, Proceedings"
  editor:
  - name: "Aart Middeldorp"
    link: "https://researchr.org/alias/aart-middeldorp"
  - name: "Taisuke Sato"
    link: "https://researchr.org/alias/taisuke-sato"
  volume: "1722"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-66677-X"
  kind: "inproceedings"
  key: "AntoyT99"
- title: "Special Issue Dedicated to ICFP 2009 Editorial"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  year: "2011"
  doi: "http://dx.doi.org/10.1017/S0956796811000190"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796811000190"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/TolmachL11"
  researchr: "https://researchr.org/publication/TolmachL11"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "21"
  number: "4-5"
  pages: "331-332"
  kind: "article"
  key: "TolmachL11"
- title: "A monadic semantics for core Curry"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Sergio Antoy"
    link: "http://web.cecs.pdx.edu/~antoy/"
  year: "2003"
  doi: "http://www.elsevier.com/gej-ng/31/29/23/135/48/show/Products/notes/index.htt#004"
  links:
    doi: "http://www.elsevier.com/gej-ng/31/29/23/135/48/show/Products/notes/index.htt#004"
  tags:
  - "semantics"
  researchr: "https://researchr.org/publication/TolmachA03"
  cites: 0
  citedby: 0
  journal: "Electronic Notes in Theoretical Computer Science"
  volume: "86"
  number: "3"
  pages: "16-34"
  kind: "article"
  key: "TolmachA03"
- title: "A Theory of Name Resolution with extended Coverage and Proofs"
  author:
  - name: "Pierre Neron"
    link: "http://www.lix.polytechnique.fr/~neron/"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  - name: "Guido Wachsmuth"
    link: "https://www.linkedin.com/in/guidowachsmuth/"
  year: "2015"
  month: "January"
  abstract: "We describe a language-independent theory for name binding and resolution, suitable for programming languages with complex scoping rules including both lexical scoping and modules. We formulate name resolution as a two stage problem. First a language-independent scope graph is constructed using language-specific rules from an abstract syntax tree. Then references in the scope graph are resolved to corresponding declarations using a language-independent resolution process. We introduce a resolution calculus as a concise, declarative, and language-independent specification of name resolution. We develop a resolution algorithm that is sound and complete with respect to the calculus. Based on the resolution calculus we develop language-independent definitions of alpha-equivalence and rename refactoring. We illustrate the approach using a small example language with modules. In addition, we show how our approach provides a model for a range of name binding patterns in existing languages."
  note: "Extended version of ESOP 2015 paper \"A Theory of Name Resolution\""
  links:
    published: "https://researchr.org/publication/NeronTVW15"
    "pdf": "http://swerl.tudelft.nl/twiki/pub/Main/TechnicalReports/TUD-SERG-2015-001.pdf"
  researchr: "https://researchr.org/publication/TUD-SERG-2015-001"
  cites: 0
  citedby: 0
  institution: "Software Engineering Research Group. Delft University of Technology"
  type: "Technical Report"
  number: "TUD-SERG-2015-001"
  kind: "techreport"
  key: "TUD-SERG-2015-001"
- title: "Scopes and Frames Improve Meta-Interpreter Specialization"
  author:
  - name: "Vlad A. Vergu"
    link: "http://www.linkedin.com/in/vladv"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2019"
  doi: "https://doi.org/10.4230/LIPIcs.ECOOP.2019.4"
  abstract: "DynSem is a domain-specific language for concise specification of the dynamic semantics of programming languages, aimed at rapid experimentation and evolution of language designs. To maintain a short definition-to-execution cycle, DynSem specifications are meta-interpreted. Meta-interpretation introduces runtime overhead that is difficult to remove by using interpreter optimization frameworks such as the Truffle/Graal Java tools; previous work has shown order-of-magnitude improvements from applying Truffle/Graal to a meta-interpreter, but this is still far slower than what can be achieved with a language-specific interpreter. In this paper, we show how specifying the meta-interpreter using scope graphs, which encapsulate static name binding and resolution information, produces much better optimization results from Truffle/Graal. Furthermore, we identify that JIT compilation is hindered by large numbers of calls between small polymorphic rules and we introduce rule cloning to derive larger monomorphic rules at run time as a countermeasure. Our contributions improve the performance of DynSem-derived interpreters to within an order of magnitude of a handwritten language-specific interpreter."
  links:
    doi: "https://doi.org/10.4230/LIPIcs.ECOOP.2019.4"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ecoop/VerguTV19"
  researchr: "https://researchr.org/publication/VerguTV19"
  cites: 0
  citedby: 0
  booktitle: "33rd European Conference on Object-Oriented Programming, ECOOP 2019, July 15-19, 2019, London, United Kingdom"
  editor:
  - name: "Alastair F. Donaldson"
    link: "https://researchr.org/alias/alastair-f.-donaldson"
  volume: "134"
  series: "LIPIcs"
  publisher: "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik"
  isbn: "978-3-95977-111-5"
  kind: "inproceedings"
  key: "VerguTV19"
- title: "A Constraint Language for Static Semantic Analysis based on Scope Graphs with Proofs"
  author:
  - name: "Hendrik van Antwerpen"
    link: "https://nl.linkedin.com/in/hendrikvanantwerpen"
  - name: "Pierre Néron"
    link: "https://researchr.org/profile/pierrejeanmichelneron/publications"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  - name: "Guido Wachsmuth"
    link: "https://www.linkedin.com/in/guidowachsmuth/"
  year: "2015"
  month: "September"
  abstract: "In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs—such as record field access—for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records."
  note: "Available at \\url{http://swerl.tudelft.nl/twiki/pub/Main/TechnicalReports/TUD-SERG-2015-009.pdf}"
  links:
    "pdf": "http://swerl.tudelft.nl/twiki/pub/Main/TechnicalReports/TUD-SERG-2015-009.pdf"
  researchr: "https://researchr.org/publication/TUD-SERG-2015-009"
  cites: 0
  citedby: 0
  institution: "Software Engineering Research Group, Delft University of Technology"
  number: "TUD-SERG-2015-009"
  kind: "techreport"
  key: "TUD-SERG-2015-009"
- title: "Intrinsically-typed definitional interpreters for imperative languages"
  author:
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Arjen Rouvoet"
    link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Robbert Krebbers"
    link: "https://robbertkrebbers.nl"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2018"
  doi: "http://doi.acm.org/10.1145/3158104"
  abstract: " 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). "
  links:
    doi: "http://doi.acm.org/10.1145/3158104"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/PoulsenRTKV18"
    technicalreport: "https://researchr.org/publication/preprint-PoulsenRTKV18"
  tags:
  - "Intrinsic-Verification"
  researchr: "https://researchr.org/publication/PoulsenRTKV18"
  cites: 0
  citedby: 0
  journal: "Proceedings of the ACM on Programming Languages"
  volume: "2"
  number: "POPL"
  kind: "article"
  key: "PoulsenRTKV18"
- title: "Optimizing ML Using a Hierarchy of Monadic Types"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "1998"
  doi: "http://link.springer.de/link/service/series/0558/bibs/1473/14730097.htm"
  links:
    doi: "http://link.springer.de/link/service/series/0558/bibs/1473/14730097.htm"
  tags:
  - "optimization"
  researchr: "https://researchr.org/publication/Tolmach98"
  cites: 0
  citedby: 0
  pages: "97-115"
  booktitle: "Types in Compilation, Second International Workshop, TIC  98, Kyoto, Japan, March 25-27, 1998, Proceedings"
  editor:
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  - name: "Atsushi Ohori"
    link: "https://researchr.org/alias/atsushi-ohori"
  volume: "1473"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "3-540-64925-5"
  kind: "inproceedings"
  key: "Tolmach98"
- title: "Bridging the Gulf: A Common Intermediate Language for ML and Haskell"
  author:
  - name: "Simon L. Peyton Jones"
    link: "http://research.microsoft.com/en-us/people/simonpj/"
  - name: "Mark Shields"
    link: "https://researchr.org/alias/mark-shields"
  - name: "John Launchbury"
    link: "https://researchr.org/alias/john-launchbury"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "1998"
  doi: "http://doi.acm.org/10.1145/268946.268951"
  links:
    doi: "http://doi.acm.org/10.1145/268946.268951"
  tags:
  - "Haskell"
  researchr: "https://researchr.org/publication/JonesSLT98"
  cites: 0
  citedby: 0
  pages: "49-61"
  booktitle: "Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages"
  address: "New York, NY, USA"
  publisher: "ACM"
  kind: "inproceedings"
  key: "JonesSLT98"
- title: "A Language Designer's Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs"
  author:
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  - name: "Guido Wachsmuth"
    link: "https://www.linkedin.com/in/guidowachsmuth/"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Pierre Néron"
    link: "https://researchr.org/profile/pierrejeanmichelneron/publications"
  - name: "Vlad A. Vergu"
    link: "http://www.linkedin.com/in/vladv"
  - name: "Augusto Passalaqua"
    link: "http://www.linkedin.com/pub/augusto-passalaqua/9/829/b29"
  - name: "Gabriël Konat"
    link: "http://nl.linkedin.com/in/gabrielkonat"
  year: "2014"
  doi: "http://doi.acm.org/10.1145/2661136.2661149"
  abstract: "The realization of a language design requires multiple artifacts that redundantly encode the same information. This entails significant effort for language implementors, and often results in late detection of errors in language definitions. In this paper we present a proof-of-concept language designer's workbench that supports generation of IDEs, interpreters, and verification infrastructure from a single source. This constitutes a first milestone on the way to a system that fully automates language implementation and verification. "
  links:
    doi: "http://doi.acm.org/10.1145/2661136.2661149"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/oopsla/VisserWTNVPK14"
    "pdf": "http://dl.acm.org/ft_gateway.cfm?id=2661149&ftid=1505232&dwn=1&CFID=550125770&CFTOKEN=54358949"
  researchr: "https://researchr.org/publication/VisserOnward14"
  cites: 0
  citedby: 0
  pages: "95-111"
  booktitle: "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"
  editor:
  - name: "Andrew P. Black"
    link: "https://researchr.org/alias/andrew-p.-black"
  - name: "Shriram Krishnamurthi"
    link: "http://www.cs.brown.edu/~sk/"
  - name: "Bernd Bruegge"
    link: "https://researchr.org/alias/bernd-bruegge"
  - name: "Joseph N. Ruskiewicz"
    link: "https://researchr.org/alias/joseph-n.-ruskiewicz"
  publisher: "ACM"
  isbn: "978-1-4503-3210-1"
  kind: "inproceedings"
  key: "VisserOnward14"
- title: "Suppl: A Flexible Language for Policies"
  author:
  - name: "Robert Dockins"
    link: "https://researchr.org/alias/robert-dockins"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2014"
  doi: "http://dx.doi.org/10.1007/978-3-319-12736-1_10"
  links:
    doi: "http://dx.doi.org/10.1007/978-3-319-12736-1_10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/aplas/DockinsT14"
  researchr: "https://researchr.org/publication/DockinsT14"
  cites: 0
  citedby: 0
  pages: "176-195"
  booktitle: "Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings"
  editor:
  - name: "Jacques Garrigue"
    link: "https://researchr.org/alias/jacques-garrigue"
  volume: "8858"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-319-12735-4"
  kind: "inproceedings"
  key: "DockinsT14"
- title: "Tag-Free Garbage Collection Using Explicit Type Parameters"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "1994"
  doi: "http://doi.acm.org/10.1145/182409.182411"
  links:
    doi: "http://doi.acm.org/10.1145/182409.182411"
  tags:
  - "tagging"
  researchr: "https://researchr.org/publication/Tolmach94"
  cites: 0
  citedby: 0
  pages: "1-11"
  booktitle: "LISP and Functional Programming"
  kind: "inproceedings"
  key: "Tolmach94"
- title: "Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)"
  author:
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Pierre Néron"
    link: "https://researchr.org/profile/pierrejeanmichelneron/publications"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2016"
  doi: "http://dx.doi.org/10.4230/DARTS.2.1.10"
  abstract: "Our paper introduces a systematic approach to the alignment of names in the static structure of a program, and memory layout and access during its execution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection. This Coq artifact showcases how our uniform model for memory layout in dynamic semantics provides structure to type soundness proofs. The artifact contains type soundness proofs mechanized in Coq for (supersets of) all languages in the paper. The type soundness proofs rely on a language-independent framework formalizing scope graphs and frame heaps."
  links:
    doi: "http://dx.doi.org/10.4230/DARTS.2.1.10"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/darts/PoulsenNTV16"
  researchr: "https://researchr.org/publication/PoulsenNTV16Artifact"
  cites: 0
  citedby: 0
  journal: "DARTS"
  volume: "2"
  number: "1"
  kind: "article"
  key: "PoulsenNTV16Artifact"
- title: "Language-Independent Type-Dependent Name Resolution"
  author:
  - name: "Hendrik van Antwerpen"
    link: "https://nl.linkedin.com/in/hendrikvanantwerpen"
  - name: "Pierre Néron"
    link: "https://researchr.org/profile/pierrejeanmichelneron/publications"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  - name: "Guido Wachsmuth"
    link: "https://www.linkedin.com/in/guidowachsmuth/"
  year: "2015"
  month: "July"
  abstract: "We extend and combine two existing declarative formalisms, the scope graphs of Neron et al. and type constraint systems, to build a language-independent theory that can describe both name and type resolution for realistic languages with complex scope and typing rules. Unlike conventional static semantics presentations, our approach maintains a clear separation between scoping and typing concerns, while still be- ing able to handle language constructs, such as class field access, for which name and type resolution are necessarily intertwined. We define a constraint scheme that can express both typing and name binding constraints, and give a for- mal notion of constraint satisfiability together with a sound algorithm for finding solutions in important special cases. We describe the details of constraint generation for a model language that illustrates many of the interesting resolution issues associated with modules, classes, and records. Our constraint generator and solver have been implemented in the Spoofax Language Workbench."
  links:
    "pdf": "http://swerl.tudelft.nl/twiki/pub/Main/TechnicalReports/TUD-SERG-2015-006.pdf"
  researchr: "https://researchr.org/publication/TUD-SERG-2015-006"
  cites: 0
  citedby: 0
  institution: "Delft University of Technology, Software Engineering Research Group"
  number: "TUD-SERG-2015-006"
  address: "Delft, The Netherlands"
  kind: "techreport"
  key: "TUD-SERG-2015-006"
- title: "A verified information-flow architecture"
  author:
  - name: "Arthur Azevedo de Amorim"
    link: "https://researchr.org/alias/arthur-azevedo-de-amorim"
  - name: "Nathan Collins"
    link: "https://researchr.org/alias/nathan-collins"
  - name: "André DeHon"
    link: "https://researchr.org/alias/andr%C3%A9-dehon"
  - name: "Delphine Demange"
    link: "https://researchr.org/alias/delphine-demange"
  - name: "Catalin Hritcu"
    link: "https://researchr.org/alias/catalin-hritcu"
  - name: "David Pichardie"
    link: "https://researchr.org/alias/david-pichardie"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "Randy Pollack"
    link: "https://researchr.org/alias/randy-pollack"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2016"
  doi: "http://dx.doi.org/10.3233/JCS-15784"
  links:
    doi: "http://dx.doi.org/10.3233/JCS-15784"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jcs/AmorimCDDHPPPT16"
  researchr: "https://researchr.org/publication/AmorimCDDHPPPT16"
  cites: 0
  citedby: 0
  journal: "Journal of Computer Security"
  volume: "24"
  number: "6"
  pages: "689-734"
  kind: "article"
  key: "AmorimCDDHPPPT16"
- title: "Procs and Locks: A Portable Multiprocessing Platform for Standard ML of New Jersey"
  author:
  - name: "J. Gregory Morrisett"
    link: "https://researchr.org/alias/j.-gregory-morrisett"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "1993"
  researchr: "https://researchr.org/publication/MorrisettT93"
  cites: 0
  citedby: 0
  pages: "198-207"
  booktitle: "PPOPP"
  kind: "inproceedings"
  key: "MorrisettT93"
- title: "Debugging Standard ML Without Reverse Engineering"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1990"
  doi: "http://doi.acm.org/10.1145/91556.91564"
  links:
    doi: "http://doi.acm.org/10.1145/91556.91564"
  tags:
  - "reverse engineering"
  - "debugging"
  researchr: "https://researchr.org/publication/TolmachA90"
  cites: 0
  citedby: 0
  pages: "1-12"
  booktitle: "LISP and Functional Programming"
  kind: "inproceedings"
  key: "TolmachA90"
- title: "Modular lazy search for Constraint Satisfaction Problems"
  author:
  - name: "Thomas Nordin"
    link: "https://researchr.org/alias/thomas-nordin"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2001"
  tags:
  - "laziness"
  - "constraints"
  - "search"
  researchr: "https://researchr.org/publication/NordinT01"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "11"
  number: "5"
  pages: "557-587"
  kind: "article"
  key: "NordinT01"
- title: "A Theory of Name Resolution"
  author:
  - name: "Pierre Néron"
    link: "https://researchr.org/profile/pierrejeanmichelneron/publications"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  - name: "Guido Wachsmuth"
    link: "https://www.linkedin.com/in/guidowachsmuth/"
  year: "2015"
  doi: "http://dx.doi.org/10.1007/978-3-662-46669-8_9"
  abstract: "We describe a language-independent theory for name binding and resolution, suitable for programming languages with complex scoping rules including both lexical scoping and modules. We formulate name resolution as a two-stage problem. First a language-independent scope graph is constructed using language-specific rules from an abstract syntax tree. Then references in the scope graph are resolved to corresponding declarations using a language-independent resolution process. We introduce a resolution calculus as a concise, declarative, and languageindependent specification of name resolution. We develop a resolution algorithm that is sound and complete with respect to the calculus. Based on the resolution calculus we develop language-independent definitions of α-equivalence and rename refactoring. We illustrate the approach using a small example language with modules. In addition, we show how our approach provides a model for a range of name binding patterns in existing languages."
  links:
    doi: "http://dx.doi.org/10.1007/978-3-662-46669-8_9"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/NeronTVW15"
    technicalreport: "https://researchr.org/publication/TUD-SERG-2015-001"
  researchr: "https://researchr.org/publication/NeronTVW15"
  cites: 0
  citedby: 0
  pages: "205-231"
  booktitle: "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"
  editor:
  - name: "Jan Vitek"
    link: "https://researchr.org/alias/jan-vitek"
  volume: "9032"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-662-46668-1"
  kind: "inproceedings"
  key: "NeronTVW15"
- title: "Building Program Optimizers with Rewriting Strategies"
  author:
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  - name: "Zine-El-Abidine Benaissa"
    link: "http://web.archive.org/web/20010515202744/www.cse.ogi.edu/~benaissa/"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "1998"
  doi: "http://doi.acm.org/10.1145/289423.289425"
  abstract: "We describe a language for defining term rewriting strategies, and its application to the production of program optimizers. Valid transformations on program terms can be described by a set of rewrite rules; rewriting strategies are used to describe when and how the various rules should be applied in order to obtain the desired optimization effects. Separating rules from strategies in this fashion makes it easier to reason about the behavior of the optimizer as a whole, compared to traditional monolithic optimizer implementations. We illustrate the expressiveness of our language by using it to describe a simple optimizer for an ML-like intermediate representation.The basic strategy language uses operators such as sequential composition, choice, and recursion to build transformers from a set of labeled unconditional rewrite rules. We also define an extended language in which the side-conditions and contextual rules that arise in realistic optimizer specifications can themselves be expressed as strategy-driven rewrites. We show that the features of the basic and extended languages can be expressed by breaking down the rewrite rules into their primitive building blocks, namely matching and building terms in variable binding environments. This gives us a low-level core language which has a clear semantics, can be implemented straightforwardly and can itself be optimized. The current implementation generates C code from a strategy specification. "
  links:
    doi: "http://doi.acm.org/10.1145/289423.289425"
    "postscript": "http://www.st.ewi.tudelft.nl/~eelco/papers/VBT98.ps"
  tags:
  - "programming languages"
  - "optimization"
  - "semantics"
  - "rule-based"
  - "meta programming"
  - "graph transformation"
  - "variable binding"
  - "Stratego/XT"
  - "transformation language"
  - "term rewriting"
  - "composition"
  - "graph-rewriting"
  - "rules"
  - "C++"
  - "program optimization"
  - "Meta-Environment"
  - "higher-order transformations"
  - "rewriting"
  - "rewriting strategies"
  - "transformation"
  - "Stratego"
  - "program transformation"
  researchr: "https://researchr.org/publication/VisserBT98"
  cites: 0
  citedby: 5
  pages: "13-26"
  booktitle: "Proceedings of the third ACM SIGPLAN international conference on Functional programming"
  editor:
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  - name: "Paul Hudak"
    link: "http://www.cs.yale.edu/homes/hudak/"
  - name: "Christian Queinnec"
    link: "https://researchr.org/alias/christian-queinnec"
  address: "Baltimore, Maryland, United States"
  publisher: "ACM"
  kind: "inproceedings"
  key: "VisserBT98"
- title: "Micro-Policies: Formally Verified, Tag-Based Security Monitors"
  author:
  - name: "Arthur Azevedo de Amorim"
    link: "https://researchr.org/alias/arthur-azevedo-de-amorim"
  - name: "Maxime Dénès"
    link: "https://researchr.org/alias/maxime-d%C3%A9n%C3%A8s"
  - name: "Nick Giannarakis"
    link: "https://researchr.org/alias/nick-giannarakis"
  - name: "Catalin Hritcu"
    link: "https://researchr.org/alias/catalin-hritcu"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  - name: "Antal Spector-Zabusky"
    link: "https://researchr.org/alias/antal-spector-zabusky"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2015"
  doi: "http://dx.doi.org/10.1109/SP.2015.55"
  links:
    doi: "http://dx.doi.org/10.1109/SP.2015.55"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sp/AmorimDGHPST15"
  researchr: "https://researchr.org/publication/AmorimDGHPST15"
  cites: 0
  citedby: 0
  pages: "813-830"
  booktitle: "2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015"
  publisher: "IEEE Computer Society"
  isbn: "978-1-4673-6949-7"
  kind: "inproceedings"
  key: "AmorimDGHPST15"
- title: "A Debugger for Standard ML"
  author:
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Andrew W. Appel"
    link: "http://www.cs.princeton.edu/~appel/"
  year: "1995"
  tags:
  - "debugging"
  researchr: "https://researchr.org/publication/TolmachA95"
  cites: 0
  citedby: 0
  journal: "Journal of Functional Programming"
  volume: "5"
  number: "2"
  pages: "155-200"
  kind: "article"
  key: "TolmachA95"
- title: "A certified framework for compiling and executing garbage-collected languages"
  author:
  - name: "Andrew McCreight"
    link: "http://web.cecs.pdx.edu/~mccreigh/"
  - name: "Tim Chevalier"
    link: "https://researchr.org/alias/tim-chevalier"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  year: "2010"
  doi: "http://doi.acm.org/10.1145/1863543.1863584"
  abstract: "We describe the design, implementation, and use of a machine-certified framework for correct compilation and execution of programs in garbage-collected languages. Our framework extends Leroy's Coq-certified Compcert compiler and Cminor intermediate language. We add: (i) a new intermediate language, GCminor, that includes primitives for allocating memory in a garbage-collected heap and for specifying GC roots; (ii) a precise, low-level specification for a Cminor library for garbage collection; and (iii) a proven semantics-preserving translation from GCminor to Cminor plus the GC library. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verification, including full semantics preservation, type preservation, or informal trust. As an example application of our framework, we describe a compiler for Haskell that translates the Glasgow Haskell Compiler's Core intermediate language to GCminor. To support a simple but useful memory safety argument for this compiler, the front end uses a novel combination of type preservation and runtime checks, which is of independent interest. "
  links:
    doi: "http://doi.acm.org/10.1145/1863543.1863584"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/McCreightCT10"
  tags:
  - "programming languages"
  - "semantics"
  - "translation"
  - "application framework"
  - "program verification"
  - "language design"
  - "Haskell"
  - "source-to-source"
  - "type checking"
  - "compiler"
  - "design"
  - "open-source"
  researchr: "https://researchr.org/publication/McCreightCT10"
  cites: 37
  citedby: 0
  pages: "273-284"
  booktitle: "Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010"
  editor:
  - name: "Paul Hudak"
    link: "https://researchr.org/alias/paul-hudak"
  - name: "Stephanie Weirich"
    link: "https://researchr.org/alias/stephanie-weirich"
  publisher: "ACM"
  isbn: "978-1-60558-794-3"
  kind: "inproceedings"
  key: "McCreightCT10"
- title: "Intrinsically-typed definitional interpreters for imperative languages"
  author:
  - name: "Casper Bach Poulsen"
    link: "http://www.casperbp.net"
  - name: "Arjen Rouvoet"
    link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  - name: "Robbert Krebbers"
    link: "https://robbertkrebbers.nl"
  - name: "Eelco Visser"
    link: "http://eelcovisser.org"
  year: "2018"
  abstract: " 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). "
  links:
    published: "https://researchr.org/publication/PoulsenRTKV18"
  researchr: "https://researchr.org/publication/preprint-PoulsenRTKV18"
  cites: 0
  citedby: 0
  type: "Preprint"
  kind: "techreport"
  key: "preprint-PoulsenRTKV18"
- title: "Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009"
  year: "2009"
  tags:
  - "functional programming"
  - "programming"
  researchr: "https://researchr.org/publication/icfp-2009"
  cites: 0
  citedby: 0
  booktitle: "Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009"
  conference: "ICFP"
  editor:
  - name: "Graham Hutton"
    link: "https://researchr.org/alias/graham-hutton"
  - name: "Andrew P. Tolmach"
    link: "http://www.cs.pdx.edu/~apt"
  publisher: "ACM"
  isbn: "978-1-60558-332-7"
  kind: "proceedings"
  key: "icfp-2009"