publications: - title: "From definitional interpreter to symbolic executor" author: - name: "Adrian D. Mensing" link: "https://researchr.org/alias/adrian-d.-mensing" - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2019" doi: "https://doi.org/10.1145/3358502.3361269" abstract: "Symbolic execution is a technique for automatic software validation and verification. New symbolic executors regularly appear for both existing and new languages and such symbolic executors are generally manually (re)implemented each time we want to support a new language. We propose to automatically generate symbolic executors from language definitions, and present a technique for mechanically (but as yet, manually) deriving a symbolic executor from a definitional interpreter. The idea is that language designers define their language as a monadic definitional interpreter, where the monad of the interpreter defines the meaning of branch points. Developing a symbolic executor for a language is a matter of changing the monadic interpretation of branch points. In this paper, we illustrate the technique on a language with recursive functions and pattern matching, and use the derived symbolic executor to automatically generate test cases for definitional interpreters implemented in our defined language." links: doi: "https://doi.org/10.1145/3358502.3361269" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/oopsla/MensingAPV19" researchr: "https://researchr.org/publication/MensingAPV19" cites: 0 citedby: 0 pages: "11-20" booktitle: "OOPSLA" kind: "inproceedings" key: "MensingAPV19" - title: "Intrinsically-typed definitional interpreters à la carte" author: - name: "Cas van der Rest" link: "https://researchr.org/alias/cas-van-der-rest" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Arjen Rouvoet" link: "https://researchr.org/alias/arjen-rouvoet" - name: "Eelco Visser" link: "https://researchr.org/alias/eelco-visser" - name: "Peter D. Mosses" link: "https://researchr.org/alias/peter-d.-mosses" year: "2022" doi: "https://doi.org/10.1145/3563355" links: doi: "https://doi.org/10.1145/3563355" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/RestPRVM22" researchr: "https://researchr.org/publication/RestPRVM22" cites: 0 citedby: 0 journal: "PACMPL" volume: "6" number: "OOPSLA2" pages: "1903-1932" kind: "article" key: "RestPRVM22" - 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: "Knowing When to Ask: Sound scheduling of name resolution in type checkers derived from declarative specifications (Extended Version)" author: - name: "Arjen Rouvoet" link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/" - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2020" month: "Oct" doi: "http://doi.org/10.5281/zenodo.4091445" abstract: "There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to automatically obtain type checkers from declarative programming language specifications. This moves the burden of proving correctness from a case-by-case basis for concrete languages to a single correctness proof for the specification language. This vision is obstructed by an aspect common to all programming languages: name resolution. Naming and scoping are pervasive and complex aspects of the static semantics of programming languages. Implementations of type checkers for languages with name binding features such as modules, imports, classes, and inheritance interleave collection of binding information (i.e., declarations, scoping structure, and imports) and querying that information. This requires scheduling those two aspects in such a way that query answers are stable---i.e., they are computed only after all relevant binding structure has been collected. Type checkers for concrete languages accomplish stability using language-specific knowledge about the type system. In this paper we give a language-independent characterization of necessary and sufficient conditions to guarantee stability of name and type queries during type checking in terms of critical edges in an incomplete scope graph. We use critical edges to give a formal small-step operational semantics to a declarative specification language for type systems, that achieves soundness by delaying queries that may depend on missing information. This yields type checkers for the specified languages that are sound by construction---i.e., they schedule queries so that the answers are stable, and only accept programs that are name- and type-correct according to the declarative language specification. We implement this approach, and evaluate it against specifications of a small module and record language, as well as subsets of Java and Scala." links: doi: "http://doi.org/10.5281/zenodo.4091445" successor: "https://researchr.org/publication/RouvoetAPKV20" researchr: "https://researchr.org/publication/RouvoetAPKV20-ext" cites: 0 citedby: 0 publisher: "Zenodo" kind: "inbook" key: "RouvoetAPKV20-ext" - title: "Scopes as types" author: - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Arjen Rouvoet" link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2018" doi: "https://doi.org/10.1145/3276484" abstract: "Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java." links: doi: "https://doi.org/10.1145/3276484" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/AntwerpenPRV18" researchr: "https://researchr.org/publication/AntwerpenPRV18" cites: 0 citedby: 0 journal: "PACMPL" volume: "2" number: "OOPSLA" kind: "article" key: "AntwerpenPRV18" - title: "Generating Specialized Interpreters for Modular Structural Operational Semantics" author: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Peter D. Mosses" link: "https://pdmosses.github.io" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-319-14125-1_13" links: doi: "http://dx.doi.org/10.1007/978-3-319-14125-1_13" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lopstr/PoulsenM13" researchr: "https://researchr.org/publication/PoulsenM13" cites: 0 citedby: 0 pages: "220-236" booktitle: "LOPSTR" kind: "inproceedings" key: "PoulsenM13" - title: "Compositional soundness proofs of abstract interpreters" author: - name: "Sven Keidel" link: "https://researchr.org/alias/sven-keidel" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Sebastian Erdweg" link: "http://www.informatik.uni-marburg.de/~seba/" year: "2018" doi: "https://doi.org/10.1145/3236767" links: doi: "https://doi.org/10.1145/3236767" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/KeidelPE18" researchr: "https://researchr.org/publication/KeidelPE18" cites: 0 citedby: 0 journal: "PACMPL" volume: "2" number: "ICFP" kind: "article" key: "KeidelPE18" - 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: "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: "PACMPL" volume: "2" number: "POPL" kind: "article" key: "PoulsenRTKV18" - title: "Generating Specialized Interpreters for Modular Structural Operational Semantics" author: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Peter D. Mosses" link: "https://pdmosses.github.io" year: "2013" links: "pdf": "http://cs.swan.ac.uk/~cscbp/lopstr13/lopstr13.pdf" "slides": "http://cs.swan.ac.uk/~cscbp/lopstr13/lopstr13_slides.pdf" "extra material": "http://cs.swan.ac.uk/~cscbp/lopstr13/index.html" researchr: "https://researchr.org/publication/BPM13" cites: 0 citedby: 0 booktitle: "Proceedings of the 23rd international symposium on Logic Based Program Synthesis and Transformation" kind: "inproceedings" key: "BPM13" - 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: "ECOOP" kind: "inproceedings" key: "PoulsenNTV16" - title: "Knowing When to Ask: Artifact" author: - name: "Arjen Rouvoet" link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/" - name: "Hendrik van Antwerpen" link: "https://researchr.org/alias/hendrik-van-antwerpen" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Robbert Krebbers" link: "https://researchr.org/alias/robbert-krebbers" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2020" month: "oct" doi: "https://doi.org/10.5281/zenodo.4068065" links: doi: "https://doi.org/10.5281/zenodo.4068065" "url": "https://doi.org/10.5281/zenodo.4068065" researchr: "https://researchr.org/publication/RouvoetAPKV20-artifact" cites: 0 citedby: 0 version: "1.0" kind: "software" key: "RouvoetAPKV20-artifact" - title: "Intrinsically-typed definitional interpreters for linear, session-typed languages" author: - name: "Arjen Rouvoet" link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2020" doi: "https://doi.org/10.1145/3372885.3373818" abstract: "An 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 often results in definitions that are cluttered with manual proof work. For linearly-typed languages (including session-typed languages) one has to prove that the interpreter, as well as all the operations on semantic components, treat values linearly. We present new methods and tools that make it possible to implement intrinsically-typed definitional interpreters for linearly-typed languages in a way that hides the majority of the manual proof work. Inspired by separation logic, we develop reusable and composable abstractions for programming with linear operations using dependent types. Using these abstractions, we define interpreters for linear lambda calculi with strong references, concurrency, and session-typed communication in Agda." links: doi: "https://doi.org/10.1145/3372885.3373818" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/RouvoetPKV20" researchr: "https://researchr.org/publication/RouvoetPKV20" cites: 0 citedby: 0 pages: "284-298" booktitle: "CPP" kind: "inproceedings" key: "RouvoetPKV20" - 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: "Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications" author: - name: "Arjen Rouvoet" link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/" - name: "Hendrik van Antwerpen" link: "https://researchr.org/alias/hendrik-van-antwerpen" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Robbert Krebbers" link: "https://researchr.org/alias/robbert-krebbers" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2020" doi: "https://doi.org/10.1145/3428248" abstract: "There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to automatically obtain type checkers from declarative programming language specifications. This moves the burden of proving correctness from a case-by-case basis for concrete languages to a single correctness proof for the specification language. This vision is obstructed by an aspect common to all programming languages: name resolution. Naming and scoping are pervasive and complex aspects of the static semantics of programming languages. Implementations of type checkers for languages with name binding features such as modules, imports, classes, and inheritance interleave collection of binding information (i.e., declarations, scoping structure, and imports) and querying that information. This requires scheduling those two aspects in such a way that query answers are stable—i.e., they are computed only after all relevant binding structure has been collected. Type checkers for concrete languages accomplish stability using language-specific knowledge about the type system. In this paper we give a language-independent characterization of necessary and sufficient conditions to guarantee stability of name and type queries during type checking in terms of critical edges in an incomplete scope graph. We use critical edges to give a formal small-step operational semantics to a declarative specification language for type systems, that achieves soundness by delaying queries that may depend on missing information. This yields type checkers for the specified languages that are sound by construction—i.e., they schedule queries so that the answers are stable, and only accept programs that are name- and type-correct according to the declarative language specification. We implement this approach, and evaluate it against specifications of a small module and record language, as well as subsets of Java and Scala." links: doi: "https://doi.org/10.1145/3428248" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/RouvoetAPKV20" researchr: "https://researchr.org/publication/RouvoetAPKV20" cites: 0 citedby: 0 journal: "PACMPL" volume: "4" number: "OOPSLA" kind: "article" key: "RouvoetAPKV20" - title: "Language-parametric static semantic code completion" author: - name: "Daniël A. A. Pelsmaeker" link: "https://pelsmaeker.net/" - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2022" doi: "https://doi.org/10.1145/3527329" links: doi: "https://doi.org/10.1145/3527329" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/PelsmaekerAPV22" researchr: "https://researchr.org/publication/PelsmaekerAPV22" cites: 0 citedby: 0 journal: "PACMPL" volume: "6" number: "OOPSLA" pages: "1-30" kind: "article" key: "PelsmaekerAPV22" - title: "Flag-based big-step semantics" author: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Peter D. Mosses" link: "https://pdmosses.github.io" year: "2017" doi: "http://dx.doi.org/10.1016/j.jlamp.2016.05.001" links: doi: "http://dx.doi.org/10.1016/j.jlamp.2016.05.001" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jlp/PoulsenM17" researchr: "https://researchr.org/publication/PoulsenM17" cites: 0 citedby: 0 journal: "jlp" volume: "88" pages: "174-190" kind: "article" key: "PoulsenM17" - title: "Imperative Polymorphism by Store-Based Types as Abstract Interpretations" author: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Peter D. Mosses" link: "https://pdmosses.github.io" - name: "Paolo Torrini" link: "https://researchr.org/alias/paolo-torrini" year: "2015" doi: "http://doi.acm.org/10.1145/2678015.2682545" links: doi: "http://doi.acm.org/10.1145/2678015.2682545" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pepm/PoulsenMT15" researchr: "https://researchr.org/publication/PoulsenMT15" cites: 0 citedby: 0 pages: "3-8" booktitle: "PEPM" kind: "inproceedings" key: "PoulsenMT15" - title: "Deriving Pretty-Big-Step Semantics from Small-Step Semantics" author: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Peter D. Mosses" link: "https://pdmosses.github.io" year: "2014" doi: "http://dx.doi.org/10.1007/978-3-642-54833-8_15" links: doi: "http://dx.doi.org/10.1007/978-3-642-54833-8_15" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/PoulsenM14" researchr: "https://researchr.org/publication/PoulsenM14" cites: 0 citedby: 0 pages: "270-289" booktitle: "ESOP" kind: "inproceedings" key: "PoulsenM14" - title: "Proceedings of the 2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2020, New Orleans, LA, USA, January 20, 2020" year: "2020" doi: "https://doi.org/10.1145/3372884" links: doi: "https://doi.org/10.1145/3372884" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/pepm/2020" researchr: "https://researchr.org/publication/pepm-2020" cites: 0 citedby: 0 booktitle: "Proceedings of the 2020 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2020, New Orleans, LA, USA, January 20, 2020" conference: "PEPM" editor: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Zhenjiang Hu" link: "https://researchr.org/alias/zhenjiang-hu" publisher: "ACM" isbn: "978-1-4503-7096-7" kind: "proceedings" key: "pepm-2020"