Static type-checking allows us to detect ill-typed programs even before running them. However, the higher complexity of type systems may cause type-checker implementation to differ from their specifications. This causes bugs and makes it hard to reason about the type of systems. To close this gap between implementation and specification, a meta-language Statix was introduced. Using Statix, we can write a specification using constraints over scope graphs and terms. Successfully solving these constraints means that the program is well-typed. However, while Statix ensures that the implementation and specification correspond to each other, it does not offer a way for its users to formally reason about the type systems' specifications. To this end, we introduce a library called statix-in-agda. This library, written using the proof assistant Agda, includes the formalisation of scope graphs and embedding of Statix's constraints. We show how we can use our library to specify the type system of STLC-like language, prove that programs in this language are well-typed, and give type-preservation proof for a type system of a simple toy language with numbers and addition.

The Statix meta-language has been developed in order to simplify the definition of static semantics in programming languages. A high-level static semantics definition of a language in Statix can be used to generate a type-checker, hence abstracting over the shared implementation details. Statix should be able to express the static semantics of itself as well. The process of defining a language using itself is called bootstrapping. In this thesis we discuss the bootstrapping of the Statix meta-language within the Spoofax language workbench. The bootstrapping of a type-system domain specific language hasn't previously been discussed in existing work. It acts as an interesting case study on the use of Statix to define semantics for a constraint-based declarative language as well as the use of Statix throughout a full compiler pipeline. In addition bootstrapping grants Statix a more expressive type system, which enables the future development of the language.

Throughout this thesis we discuss the components of the Statix compiler and explain how these changed as part of the bootstrapping process. The correctness is validated by comparing compiled specifications of the bootstrapped compiler and the existing reference solution for alpha equivalence. We also provide a brief indication of the performance of the bootstrapped Statix compiler.

The bootstrapped compiler is believed to be correct, but does currently not perform to the desired standard. The compiler is successful on smaller language projects, but has a massive growth in compile time when it is used on larger, more complex language projects. This means future work is needed in order for it to be incorporated into the language workbench.

Static type systems can greatly enhance the quality of programs, but implementing a type checker for them is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make this task easier by automatically deriving a type checker from a declarative specification of the type system. However, so far Statix has not been used to implement a type system with dependent types, an expressive class of type systems which require evaluation of terms during type checking.

In this thesis, we present a specification of a simple dependently typed language in Statix, and discuss how to extend it with several common features such as inductive data types, universes, and inference of implicit arguments. While we encountered some challenges in the implementation, our conclusion is that Statix is already usable as a tool for implementing dependent types.

This paper investigates the viability of using scope graphs to implement type checkers for programming languages, specifically for a Scala subset. The primary objective is to determine if scope graphs can offer a declarative and extensible approach to type checking. To achieve this, we used a phased Haskell library to implement such a type checker. The declarativity and feature extensibility of the approach were evaluated by means of comparation with Rouvoet et al.'s approach in mini-Statix. The results demonstrate that using scope graphs as a basis for type checking yields a modular and extensible solution compared to traditional methods. However, it is noted that this approach may sacrifice a certain degree of declarativity. These findings suggest that scope graphs are a promising tool for type checking, particularly in the context of name binding. Further research is recommended to explore the possibility of implementing similar type checkers for other programming languages. Additionally, the paper suggests incorporating additional features into the targeted Scala subset, thereby enhancing its extensibility.

Substructural typing imposes additional constraints on variable usage during type checking and requires specialized approaches to ensure type soundness. In this study, we investigate the implementation of a type checker using scope graphs for languages with substructural type systems. Scope graphs, a data structure representing scoping, provide a foundation for defining type checking algorithms. Our research project extends an existing Haskell library, incorporating typing rules for non-substructural, linear, and affine type systems. Through careful examination and comparison of scope graph and calculus implementations, we evaluate their expressiveness, extensibility, and readability. While the scope graph implementation demonstrates promising results, passing all test cases, the calculus implementation encounters unification errors in a subset of the tests. We conclude that the scope graph implementation offers a solid foundation for substructural typing, with potential for easy extension and integration with other language features. However, further work is needed to develop a comprehensive test suite and address the challenges faced by the calculus implementation. By advancing these areas, we can enhance the effectiveness of substructural type checking and enable more reliable and secure programming practices in languages with substructural type systems.

In this paper, we explore scope graphs as a formal model for constructing type checkers for programming languages that support type classes. Type classes provide a powerful mechanism for ad hoc-polymorphism and code reuse. Nevertheless, the incorporation of type classes into type checkers poses challenges, as it necessitates the resolution of instances and the assurance of coherence amidst overlapping instances. Our approach facilitates the separation of concerns between type class resolution and type checking, promoting extensibility and maintainability of the type checker. We contribute with a formal definition of scope graphs for languages with type classes, accompanied by algorithms for type class resolution and type checking. To assess the correctness of this approach, we implement a prototype type checker, and conduct experiments on a collection of representative programs. The results demonstrate the effectiveness of this baseline approach.

Scope graphs provide a way to type-check real-world programming languages and their constructs. A previous implementation that type-checks the proof-of-concept language LM, a language with relative, unordered, and glob imports, does not halt. This thesis discusses a five-step approach for constructing and type-checking a scope graph of an LM program. Using manually scheduled queries and auxiliary algorithms, type-checking the majority of examples failing in previous literature succeeds. The introduction of breadth-first-traversal and multi-origin querying is discussed as new scope graph primitives to aid in the reusability of this thesis for type-checkers that require stratified resolution.

A refactoring is a program transformation that improves the design of the source code, while preserving its behavior. Most modern IDEs offer a number of automated refactorings as editor services. The Rename refactoring is the most-commonly applied refactoring and is used to change the identifier of a program entity such as a variable, a function, or a type. Correctly implementing refactorings is notoriously complex and these state-of-the-art implementations are known to be faulty and too restrictive. When developing a new programming language, it is both difficult and time-consuming to implement sound and complete automated refactoring transformations. Language-parametric definitions of refactorings that can be reused by instantiation with the syntax and semantics of a language, allow the development effort of refactorings to be amortized across language implementations. In this thesis, we developed a language-parametric Rename refactoring algorithm that works on an abstract model of a program's name binding structure. We implemented the algorithm in the Spoofax language workbench, building on the language-parametric representation of name binding with scope graphs and using generic traversals in the Stratego transformation language. We evaluated the algorithm with five different languages implemented in Spoofax, which uses both NaBL2 and Statix to declare their static semantics and name binding rules. As a result, Spoofax now provides an automated Rename refactoring that works for any language developed with the language workbench using NaBL2/Statix.