publications: - 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: "Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers" author: - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2021" doi: "https://doi.org/10.4230/LIPIcs.ECOOP.2021.1" links: doi: "https://doi.org/10.4230/LIPIcs.ECOOP.2021.1" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ecoop/AntwerpenV21" researchr: "https://researchr.org/publication/AntwerpenV21" cites: 0 citedby: 0 booktitle: "35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference)" editor: - name: "Anders Møller" link: "https://researchr.org/alias/anders-m%C3%B8ller" - name: "Manu Sridharan" link: "https://researchr.org/alias/manu-sridharan" volume: "194" series: "LIPIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-190-0" kind: "inproceedings" key: "AntwerpenV21" - 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: "Proceedings of the 4th ACM SIGPLAN International Workshop on Meta-Programming Techniques and Reflection, META@SPLASH 2019, Athens, Greece, October 20, 2019" editor: - name: "Christophe Scholliers" link: "https://researchr.org/alias/christophe-scholliers" - name: "Guido Chari" link: "https://researchr.org/alias/guido-chari" publisher: "ACM" isbn: "978-1-4503-6985-5" kind: "inproceedings" key: "MensingAPV19" - title: "Towards language-parametric semantic editor services based on declarative type system specifications" author: - name: "Daniël A. A. Pelsmaeker" link: "https://pelsmaeker.net/" - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2019" doi: "https://doi.org/10.1145/3359061.3362782" abstract: "New programming languages often lack good IDE support, as developing advanced semantic editor services takes additional effort. In previous work we discussed the operational requirements of a constraint solver that leverages the declarative type system specification of a language to provide language-parametric semantic editor services. In this work we describe the implementation of our solver as a two stage process: inference and search. An editor-service specific search strategy determines how and where the search is conducted, and when it terminates. We are currently implementing and evaluating this idea." links: doi: "https://doi.org/10.1145/3359061.3362782" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/oopsla/PelsmaekerAV19" researchr: "https://researchr.org/publication/PelsmaekerAV19-SPLASH" cites: 0 citedby: 0 pages: "19-20" booktitle: "Proceedings Companion of the 2019 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, SPLASH 2019, Athens, Greece, October 20-25, 2019" editor: - name: "Yannis Smaragdakis" link: "https://researchr.org/alias/yannis-smaragdakis" publisher: "ACM" isbn: "978-1-4503-6992-3" kind: "inproceedings" key: "PelsmaekerAV19-SPLASH" - 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: "Dynamic Data-Driven Experiments in the Smart Grid Domain with a Multi-agent Platform" author: - name: "Zülküf Genç" link: "https://researchr.org/alias/z%C3%BClk%C3%BCf-gen%C3%A7" - name: "Michel A. Oey" link: "https://researchr.org/alias/michel-a.-oey" - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Frances M. T. Brazier" link: "https://researchr.org/alias/frances-m.-t.-brazier" year: "2015" doi: "http://dx.doi.org/10.1007/978-3-319-31447-1_8" links: doi: "http://dx.doi.org/10.1007/978-3-319-31447-1_8" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/mabs/GencOAB15" researchr: "https://researchr.org/publication/GencOAB15" cites: 0 citedby: 0 pages: "121-131" booktitle: "Multi-Agent-Based Simulation XVI - International Workshop, MABS 2015, Istanbul, Turkey, May 5, 2015, Revised Selected Papers" editor: - name: "Benoit Gaudou" link: "https://researchr.org/alias/benoit-gaudou" - name: "Jaime Simão Sichman" link: "https://researchr.org/alias/jaime-sim%C3%A3o-sichman" volume: "9568" series: "Lecture Notes in Computer Science" publisher: "Springer" isbn: "978-3-319-31446-4" kind: "inproceedings" key: "GencOAB15" - title: "Towards Language-Parametric Semantic Editor Services Based on Declarative Type System Specifications (Brave New Idea Paper)" author: - name: "Daniël A. A. Pelsmaeker" link: "https://pelsmaeker.net/" - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2019" doi: "https://doi.org/10.4230/LIPIcs.ECOOP.2019.26" abstract: "Editor services assist programmers to more effectively write and comprehend code. Implementing editor services correctly is not trivial. This paper focuses on the specification of semantic editor services, those that use the semantic model of a program. The specification of refactorings is a common subject of study, but many other semantic editor services have received little attention. We propose a language-parametric approach to the definition of semantic editor services, using a declarative specification of the static semantics of the programming language, and constraint solving. Editor services are specified as constraint problems, and language specifications are used to ensure correctness. We describe our approach for the following semantic editor services: reference resolution, find usages, goto subclasses, code completion, and the extract definition refactoring. We do this in the context of Statix, a constraint language for the specification of type systems. We investigate the specification of editor services in terms of Statix constraints, and the requirements these impose on a suitable solver." links: doi: "https://doi.org/10.4230/LIPIcs.ECOOP.2019.26" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ecoop/PelsmaekerAV19" researchr: "https://researchr.org/publication/PelsmaekerAV19" 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: "PelsmaekerAV19" - 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: "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: "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 Constraint-based Approach to Name Binding and Type Checking using Scope Graphs" author: - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" year: "2016" month: "January" abstract: "Recently scope graphs were introduced as a formalism to specify the name binding structure of a program and do name resolution independent of the abstract syntax tree of a program. In this thesis we show how to use a constraint language based on scope graphs to do static analysis of programs. We do this by extracting constraints from a program, that specify name binding and typing. We treat binding and typing as separate building blocks, but our approach allows language constructs – such as access of record fields – where name and type resolution are mutually dependent. By using scope graphs for name resolution, our approach supports a wide range of name binding patterns that are not easily supported in existing constraint-based approaches. We present a formal semantics for our constraint language, as well as a solver algorithm, for which we discuss soundness, termination and completeness of the solver. We evaluate our approach by expressing the static semantics of PCF and Featherweight Java with our constraints, and we implemented the solver algorithm, as well as static analysis for both languages, in the Spoofax language workbench." note: "Available at \\url{http://resolver.tudelft.nl/uuid:7a555c92-ee75-4e64-b58b-d8f09662f412}." researchr: "https://researchr.org/publication/VanAntwerpen2016" cites: 0 citedby: 0 school: "Delft University of Technology" advisor: - name: "Eelco Visser" link: "http://eelcovisser.org" kind: "mastersthesis" key: "VanAntwerpen2016" - title: "Incremental type-checking for free: using scope graphs to derive incremental type-checkers" author: - name: "Aron Zwaan" link: "https://aronzwaan.github.io" - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2022" doi: "https://doi.org/10.1145/3563303" links: doi: "https://doi.org/10.1145/3563303" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/ZwaanAV22" researchr: "https://researchr.org/publication/ZwaanAV22" cites: 0 citedby: 0 journal: "Proceedings of the ACM on Programming Languages" volume: "6" number: "OOPSLA2" pages: "424-448" kind: "article" key: "ZwaanAV22" - 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: "Proceedings of the ACM on Programming Languages" volume: "6" number: "OOPSLA" pages: "1-30" kind: "article" key: "PelsmaekerAPV22" - 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: "Proceedings of the ACM on Programming Languages" volume: "2" number: "OOPSLA" kind: "article" key: "AntwerpenPRV18" - title: "Scope Graphs: The Story so Far" author: - name: "Aron Zwaan" link: "https://aronzwaan.github.io" - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" year: "2023" doi: "https://doi.org/10.4230/OASIcs.EVCS.2023.32" links: doi: "https://doi.org/10.4230/OASIcs.EVCS.2023.32" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/birthday/ZwaanA23" researchr: "https://researchr.org/publication/ZwaanA23" cites: 0 citedby: 0 booktitle: "Eelco Visser Commemorative Symposium, EVCS 2023, April 5, 2023, Delft, The Netherlands" editor: - name: "Ralf Lämmel" link: "https://researchr.org/alias/ralf-l%C3%A4mmel" - name: "Peter D. Mosses" link: "https://researchr.org/alias/peter-d.-mosses" - name: "Friedrich Steimann" link: "https://researchr.org/alias/friedrich-steimann" volume: "109" series: "OASIcs" publisher: "Schloss Dagstuhl - Leibniz-Zentrum für Informatik" isbn: "978-3-95977-267-9" kind: "inproceedings" key: "ZwaanA23" - title: "Scope States (Artifact)" author: - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2021" doi: "https://doi.org/10.4230/DARTS.7.2.1" links: doi: "https://doi.org/10.4230/DARTS.7.2.1" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/darts/AntwerpenV21" researchr: "https://researchr.org/publication/AntwerpenV21-artifact" cites: 0 citedby: 0 journal: "DARTS" volume: "7" number: "2" kind: "article" key: "AntwerpenV21-artifact"