Name binding is an integral part of the static semantics of programming languages. Modern languages commonly feature name binding constructs, such as packages, modules, and user-defined types that are essential to develop and maintain large programs. Static reasoning about name binding is key to support many services offered by modern programming environments, from type checking, to interactive code navigation and automatic refactoring. Formal specification of a programming language is important to understand and reason about the language, as well as to implement it.

Expressive name binding features pose challenges for both high-level specifications and implementations. The first challenge is finding high-level abstractions to describe expressive name binding. The second challenge is correctly implementing high-level specifications that were not written with the goal of implementation in mind. Due to these challenges, specifications are often restricted to a core language that lacks many of the surface language's features. The surface language is only defined by the details of the lower-level implementation. Those implementations use specialized data structures and algorithms to support the full language, which limits code reuse, increases development effort, and makes it more difficult to ensure correctness.

Meta-languages aim to address these challenges and bridge the gap between high-level specification and implementation by providing reusable abstractions for common aspects of programming languages, as well as reusable implementations for specifications in the meta-language. Reusable implementations greatly reduce development effort, and their correctness has to be shown only once instead of for each individual language implementation.

This dissertation proposes a novel meta-language, Statix, for the specification of static semantics. It is based on scope graphs, a general model for name binding in programming languages (Neron et al., 2015). Statix supports the direct modeling of surface language name binding features, stays close to a familiar inference-style of specification, and allows automatically deriving implementations for compilers and editor services. This dissertation makes the following three contributions.

First, we present the design of the meta-language Statix. Statix is a logic language extended with primitives to construct and query scope graphs. Specifications are written as logical predicates that abstract over evaluation order. The design is accompanied by a declarative semantics that gives a precise description of the meaning of specifications written in the meta-language.

Second, we present an operational semantics for Statix that executes specifications in the meta-language as type checkers. We prove that the operational semantics is correct with respect to the declarative semantics. We observe that the operational semantics is incomplete, but argue based on our experience with case studies that this is rarely a problem in practice. We present a framework to implement implicitly parallelized scope-graph-based type checkers. We apply this to our Statix implementation, resulting in substantially improved runtime performance. Additionally, we propose an approach towards implementing language-parametric semantic editor services based on meta-language specifications.

Third, we implement these operational semantics and present case studies of several core languages from the literature as well as of a large subset of Java. The case studies consist of specifications and executable test suites, which allows us to evaluate both the expressiveness and the practical usability of the meta-language.

We evaluate our work by assessing whether Statix (i) has a clear and clean underlying theory (principled); (ii) can handle a broad range of common language features (expressive); (iii) is declarative, but realizable by practical algorithms and tools (executable); (iv) is factored into language-specific and language-independent parts, to maximize reuse (reusable); and (v) can be applied to erroneous programs as well as to correct ones (resilient). We conclude that our approach is sufficient to express and interpret common name binding and type system features. The approach scales to the full surface syntax of real-world programming languages. As such the meta-language fulfills criteria (i) to (iv) well, although we do identify potential improvements. Criterion (v) is only minimally met and remains an important open challenge.

Our work shows that high-level specification of surface language name binding features using a meta-language approach is feasible and useful. It allows easier specification of complete languages, and supports reusable practical implementations for those languages. The following three topics are important areas of future research. The first is to develop abstractions for language features that are currently hard or cumbersome to specify in Statix. The second is to improve the integration of Statix in development environments. This requires better handling of erroneous programs and improved error reporting. It also requires developing program representations that make static program information accessible for program transformation and compilation. The third is to develop approaches for code completion, program repair, and program generation based on Statix specifications. Further research on these topics would make this meta-language approach even more widely applicable.
@en

Static name binding (i.e., associating references with appropriate declarations) is an essential aspect of programming languages. However, it is usually treated in an unprincipled manner, often leaving a gap between formalization and implementation. The scope graph formalism mitigates these deficiencies by providing a well-defined, first-class, language-parametric representation of name binding. Scope graphs serve as a foundation for deriving type checkers from declarative type system specifications, reasoning about type soundness, and implementing editor services and refactorings. In this paper we present an overview of scope graphs, and, using examples, show how the ideas and notation of the formalism have evolved. We also briefly discuss follow-up research beyond type checking, and evaluate the formalism.

@en

Code completion is an editor service in IDEs that proposes code fragments for the user to insert at the caret position in their code. Code completion should be sound and complete. It should be sound, such that it only proposes fragments that do not violate the syntactic and static semantic rules of the language. It should be complete, such that it proposes all valid fragments so that code completion can be used to construct all programs. To realize soundness and completeness, code completion should be informed by the language definition. In practice, the implementation of code completion is an additional effort in the implementation of a language.

In this paper, we develop a framework for language-parametric semantic code completion for statically typed programming languages based on their specification of syntax and static semantics, realizing the implementation of a code completion editor service with minimal additional effort. The framework builds on the SDF3 syntax definition formalism and the Statix static semantics specification language. The algorithm reinterprets the static semantics definition to find sound expansions of predicates and solutions to name resolution queries in scope graphs. This allows a search strategy to explore the solution space and synthesize completion proposals. The implementation of the strategy language and code completion algorithm extend the implementation of the Statix solver, and can be used for any language defined in Statix. We demonstrate soundness and completeness of the completion proposal synthesis, and evaluate its performance.@en

Fast analysis response times in IDEs are essential for a good editor experience. Incremental type-checking can provide that in a scalable fashion. However, existing techniques are not reusable between languages. Moreover, mutual and dynamic dependencies preclude traditional approaches to incrementality. This makes finding automatic approaches to incremental type-checking a challenging but important open question.
In this paper, we present a technique that automatically derives incremental type-checkers from type system specifications written in the Statix meta-DSL. We use name resolution queries in scope graphs (a generic model of name binding embedded in Statix) to derive dependencies between compilation units. A novel query confirmation algorithm finds queries for which the answer changed due to an edit in the program. Only units with such queries require reanalysis. The effectiveness of this algorithm is improved by (1) splitting the type-checking task into a context-free and a context-sensitive part, and (2) reusing a generic mechanism to resolve mutual dependencies. This automatically yields incremental type-checkers for any Statix specification.
Compared to non-incremental parallel execution, we achieve speedups up to 147x on synthetic benchmarks, and up to 21x on real-world projects, with initial overheads below 10%. This suggests that our framework can provide efficient incremental type-checking to the wide range of languages supported by Statix.@en

Compilers that can type check compilation units in parallel can make more efficient use of multi-core architectures, which are nowadays widespread. Developing parallel type checker implementations is complicated by the need to handle concurrency and synchronization of parallel compilation units. Dependencies between compilation units are induced by name resolution, and a parallel type checker needs to ensure that units have defined all relevant names before other units do a lookup. Mutually recursive references and implicitly discovered dependencies between compilation units preclude determining a static compilation order for many programming languages. In this paper, we present a new framework for implementing hierarchical type checkers that provides implicit parallel execution in the presence of dynamic and mutual dependencies between compilation units. The resulting type checkers can be written without explicit handling of communication or synchronization between different compilation units. We achieve this by providing type checkers with an API for name resolution based on scope graphs, a language-independent formalism that supports a wide range of binding patterns. We introduce the notion of scope state to ensure safe name resolution. Scope state tracks the completeness of a scope, and is used to decide whether a scope graph query between compilation units must be delayed. Our framework is implemented in Java using the actor paradigm. We evaluated our approach by parallelizing the solver for Statix, a meta-language for type checkers based on scope graphs, using our framework. This parallelizes every Statix-based type checker, provided its specification follows a split declaration-type style. Benchmarks show that the approach results in speedups for the parallel Statix solver of up to 5.0x on 8 cores for real-world code bases.

@en

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.

@en

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.

@en

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.

@en

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.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.@en

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.@en

Pervasive information and communication technologies and large-scale complex systems, are strongly influencing today’s networked society. Understanding the behaviour and impact of such distributed, often emergent systems on society is of vital importance. This paper proposes a new approach to better understand the complexity of large-scale participatory systems in the context of smart grids. Multi-agent based distributed simulations of realistic multi-actor scenarios incorporating real-time dynamic data and active participation of actors is the means to this purpose. The Symphony experiment platform, developed to study complex emergent behaviours and to facilitate the analysis of the system dynamics and actor interactions, is the enabler.@en