publications: - title: "A Monadic Framework for Name Resolution in Multi-phased Type Checkers" author: - name: "Casper Bach Poulsen" link: "https://researchr.org/alias/casper-bach-poulsen" - name: "Aron Zwaan" link: "https://researchr.org/alias/aron-zwaan" - name: "Paul Hübner" link: "https://researchr.org/alias/paul-h%C3%BCbner" year: "2023" doi: "https://doi.org/10.1145/3624007.3624051" links: doi: "https://doi.org/10.1145/3624007.3624051" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/gpce/PoulsenZH23" researchr: "https://researchr.org/publication/PoulsenZH23" cites: 0 citedby: 0 pages: "14-28" booktitle: "GPCE" kind: "inproceedings" key: "PoulsenZH23" - 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: "ECOOP" kind: "inproceedings" key: "PelsmaekerAV19" - 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." 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: "Scoped Dynamic Rewrite Rules" author: - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2001" doi: "https://doi.org/10.1016/S1571-0661(04)00298-1" abstract: "The applicability of term rewriting to program transformation is limited by the lack of control over rule application and by the context-free nature of rewrite rules. The first problem is addressed by languages supporting user-definable rewriting strate- gies. This paper addresses the second problem by extending rewriting strategies with scoped dynamic rewrite rules. Dynamic rules are generated at run-time and can access variables available from their definition context. Rules generated within a rule scope are automatically retracted at the end of that scope. The technique is illustrated by means of several program tranformations: bound variable renaming, function inlining, and dead function elimination. " links: doi: "https://doi.org/10.1016/S1571-0661(04)00298-1" successor: "https://researchr.org/publication/BravenboerDOV06" tags: - "programming languages" - "rule-based" - "graph transformation" - "dynamic rewrite rules" - "Stratego/XT" - "transformation language" - "term rewriting" - "graph-rewriting" - "rules" - "context-aware" - "access control" - "rewriting" - "role-based access control" - "rewriting strategies" - "transformation" - "Stratego" - "program transformation" researchr: "https://researchr.org/publication/Visser01-DR" cites: 0 citedby: 0 journal: "ENTCS" volume: "59" number: "4" pages: "375-396" kind: "article" key: "Visser01-DR" - 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: "ECOOP" kind: "inproceedings" key: "AntwerpenV21" - 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: "ESOP" kind: "inproceedings" key: "NeronTVW15" - title: "A language generic solution for name binding preservation in refactorings" author: - name: "Maartje de Jonge" link: "https://researchr.org/profile/maartjedejonge/publications" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2012" doi: "http://doi.acm.org/10.1145/2427048.2427050" abstract: "The implementation of refactorings for new languages requires considerable effort from the language developer. We aim at reducing that effort by using language generic techniques. This paper focuses on behavior preservation, in particular the preservation of static name bindings. To detect name binding violations, we implement a technique that reuses the name analysis defined in the compiler front end. Some languages offer the possibility to access variables using qualified names. As a refinement to violation detection, we show that name analysis can be defined as a reusable traversal strategy that can be applied to restore name bindings by creating qualified names. These techniques offer an efficient and reliable solution; the semantics of the language is implemented only once, with the compiler being the single source of truth. We evaluate our approach by implementing a language generic rename refactoring, which we apply to two domain specific languages and a subset of the Java language." links: doi: "http://doi.acm.org/10.1145/2427048.2427050" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/ldta/JongeV12" researchr: "https://researchr.org/publication/JongeV12-LDTA" cites: 0 citedby: 0 pages: "2" booktitle: "LDTA" kind: "inproceedings" key: "JongeV12-LDTA" - title: "The semantics of name resolution in grace" author: - name: "Vlad A. Vergu" link: "https://researchr.org/alias/vlad-a.-vergu" - name: "Michiel Haisma" link: "https://researchr.org/alias/michiel-haisma" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2017" doi: "https://doi.org/10.1145/3133841.3133847" abstract: "Grace is a dynamic object oriented programming language designed to aid programming education. We present a formal model of and give an operational semantics for its object model and name resolution algorithm. Our main contributions are a systematic model of Grace’s name resolution using scope graphs, relating linguistic features to other languages, and an operationalization of this model in the form of an operational semantics which is readable and executable. The semantics are extensively tested against a reference Grace implementation. " links: doi: "https://doi.org/10.1145/3133841.3133847" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/dls/VerguHV17" technicalreport: "https://researchr.org/publication/TUD-SERG-2017-011" researchr: "https://researchr.org/publication/VerguHV17" cites: 0 citedby: 0 pages: "63-74" booktitle: "DLS" kind: "inproceedings" key: "VerguHV17" - 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: "Declarative Name Binding and Scope Rules" author: - name: "Gabriël Konat" link: "http://nl.linkedin.com/in/gabrielkonat" - name: "Lennart C. L. Kats" link: "http://www.lclnet.nl/" - name: "Guido Wachsmuth" link: "https://www.linkedin.com/in/guidowachsmuth/" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2012" doi: "http://dx.doi.org/10.1007/978-3-642-36089-3_18" abstract: "In textual software languages, names are used to reference elements like variables, methods, classes, etc. Name resolution analyses these names in order to establish references between definition and use sites of elements. In this paper, we identify recurring patterns for name bindings in programming languages and introduce a declarative metalanguage for the specification of name bindings in terms of namespaces, definition sites, use sites, and scopes. Based on such declarative name binding specifications, we provide a language-parametric algorithm for static name resolution during compile-time. We discuss the integration of the algorithm into the Spoofax Language Workbench and show how its results can be employed in semantic editor services like reference resolution, constraint checking, and content completion." links: doi: "http://dx.doi.org/10.1007/978-3-642-36089-3_18" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sle/KonatKWV12" researchr: "https://researchr.org/publication/KonatKWV12" cites: 0 citedby: 0 pages: "311-331" booktitle: "SLE" kind: "inproceedings" key: "KonatKWV12" - 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: "BIRTHDAY" kind: "inproceedings" key: "ZwaanA23" - title: "Program Transformation with Scoped Dynamic Rewrite Rules" author: - name: "Martin Bravenboer" link: "http://martin.bravenboer.name/" - name: "Arthur van Dam" link: "https://researchr.org/profile/arthurvandam/publications" - name: "Karina Olmos" link: "https://researchr.org/profile/karinaolmos/publications" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2006" doi: "https://content.iospress.com/articles/fundamenta-informaticae/fi69-1-2-06" abstract: "The applicability of term rewriting to program transformation is limited by the lack of control over rule application and by the context-free nature of rewrite rules. The first problem is addressed by languages supporting user-definable rewriting strategies. The second problem is addressed by the extension of rewriting strategies with scoped dynamic rewrite rules. Dynamic rules are defined at run-time and can access variables available from their definition context. Rules defined within a rule scope are automatically retracted at the end of that scope. In this paper, we explore the design space of dynamic rules, and their application to transformation problems. The technique is formally defined by extending the operational semantics underlying the program transformation language Stratego, and illustrated by means of several program transformations in Stratego, including constant propagation, bound variable renaming, dead code elimination, function inlining, and function specialization. " links: doi: "https://content.iospress.com/articles/fundamenta-informaticae/fi69-1-2-06" "technical report": "http://www.cs.uu.nl/research/techreps/UU-CS-2005-005.html" tags: - "programming languages" - "semantics" - "rule-based" - "formal semantics" - "graph transformation" - "dynamic rewrite rules" - "Stratego/XT" - "transformation language" - "term rewriting" - "language design" - "graph-rewriting" - "rules" - "operational semantics" - "context-aware" - "access control" - "rewriting" - "design" - "role-based access control" - "rewriting strategies" - "transformation" - "Stratego" - "program transformation" researchr: "https://researchr.org/publication/BravenboerDOV06" cites: 0 citedby: 4 journal: "FUIN" volume: "69" number: "1-2" pages: "123-178" kind: "article" key: "BravenboerDOV06" - 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: "PACMPL" volume: "6" number: "OOPSLA2" pages: "424-448" kind: "article" key: "ZwaanAV22" - 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: "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: "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: "ECOOP" kind: "inproceedings" key: "VerguTV19" - 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: "PEPM" kind: "inproceedings" key: "AntwerpenNTVW16" - 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." 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: "The Spoofax Name Binding Language" author: - name: "Gabriël Konat" link: "http://nl.linkedin.com/in/gabrielkonat" - name: "Vlad A. Vergu" link: "http://www.linkedin.com/in/vladv" - name: "Lennart C. L. Kats" link: "http://www.lclnet.nl/" - name: "Guido Wachsmuth" link: "https://www.linkedin.com/in/guidowachsmuth/" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2012" doi: "https://doi.org/10.1145/2384716.2384748" abstract: "In textual software languages, names are used to identify program elements such as variables, methods, and classes. Name analysis algorithms resolve names in order to establish references between definitions and uses of names. In this poster, we present the Spoofax Name Binding Language (NBL), a declarative meta-language for the specification of name binding and scope rules, which departs from the programmatic encodings of name binding provided by regular approaches. NBL aspires to become the universal language for name binding, which can be used next to BNF definitions in reference manuals, as well as serve the generation of implementations." links: doi: "https://doi.org/10.1145/2384716.2384748" "url": "https://doi.org/10.1145/2384716.2384748" tags: - "C++" - "Spoofax" researchr: "https://researchr.org/publication/KonatVKWV2012" cites: 0 citedby: 0 booktitle: "Companion to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2012, Tucson, AR, USA, October 19 - 26, 2012" kind: "inproceedings" key: "KonatVKWV2012" - title: "A Language Independent Task Engine for Incremental Name and Type Analysis" author: - name: "Guido Wachsmuth" link: "https://www.linkedin.com/in/guidowachsmuth/" - name: "Gabriël Konat" link: "http://nl.linkedin.com/in/gabrielkonat" - name: "Vlad A. Vergu" link: "http://www.linkedin.com/in/vladv" - name: "Danny M. Groenewegen" link: "https://www.linkedin.com/in/dannygroenewegen/" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-319-02654-1_15" abstract: "IDEs depend on incremental name and type analysis for responsive feedback for large projects. In this paper, we present a language-independent approach for incremental name and type analysis. Analysis consists of two phases. The first phase analyzes lexical scopes and binding instances and creates deferred analysis tasks. A task captures a single name resolution or type analysis step. Tasks might depend on other tasks and are evaluated in the second phase. Incrementality is supported on file and task level. When a file changes, only this file is recollected and only those tasks are reevaluated, which are affected by the changes in the collected data. The analysis does neither re-parse nor re-traverse unchanged files, even if they are affected by changes in other files. We implemented the approach as part of the Spoofax Language Workbench and evaluated it for the WebDSL web programming language. " links: doi: "http://dx.doi.org/10.1007/978-3-319-02654-1_15" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/sle/WachsmuthKVGV13" technicalreport: "https://researchr.org/publication/TUD-SERG-2013-018" researchr: "https://researchr.org/publication/WachsmuthKVGV13" cites: 0 citedby: 0 pages: "260-280" booktitle: "SLE" kind: "inproceedings" key: "WachsmuthKVGV13" - 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: "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: "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"