WebDSL is a DSL for creating web applications, combining many different aspects and domains of web design in a single language. The dynamic semantics of this language are not defined, despite multiple attempts, abandoned due to complexity of the language and lack of expression of chosen frameworks. We adapt the algebraic effects and handlers approach and the framework introduced in Datatypes a la carte (Swierstra, 2008) to create a modular denotational semantics model of WebDSL, extending the framework by a bifunctor formulation for multi-sort syntax definition that allows us to distinguish between effects raised by different components of the language. In the process of defining the framework and semantics in Haskell, we encountered obstacles and of working with algebraic effects and handlers paradigm in the language, leading us to compile workarounds, solutions and pitfalls to avoid when constructing and maintaining such model. In evaluation of the framework approach with earlier attempts at defining dynamic semantics for WebDSL, we find algebraic effects and handlers to be a viable and successful approach for modelling a rich DSL such as WebDSL, and propose possible improvements to the WebDSL compiler.

This thesis investigates the potential of basing a program synthesis system on a de-
pendent type theory. This is an attractive research direction because it allows a very
flexible range of specification to be expressed within the same framework. We im-
plement a prototype of a search algorithm driven by unsolved constraints typically
generated during dependent type checking. We encode a range of synthesis prob-
lems from literature in our system, showcasing how it can be used for expressing
the specification and synthesizing programs that manipulate data. We empirically
establish the effect of constraint-directed aspect of our approach on performance,
based on the encoded problems.

The process of using formal verification, in order to ensure that a piece of software meets it functional requirements consists of three main steps: designing a model of the given piece of software, translating the functional requirements, which the piece of software must satisfy, into properties of said model and verifying that the model satisfies those properties. Traditionally, regardless of whether the piece of software is developed based on a predesigned model or the piece of software is developed first and its model is designed after that, the piece of software and its model are two separate entities. Therefore, aside from checking that the model satisfies its properties, it must also be verified that the model accurately represents the given piece of software. While this task may initially seem simple, it gets progressively more difficult, as the piece of software becomes more complex. And, if it turns out that the model is not accurate, then the entire formal verification process is invalid, since it does not provide any guarantees about the actual piece of software. In this thesis we present a solution to this problem: a way of modelling sequential effectful programs, such that the resulting models can be directly translated into runnable programs, thereby guaranteeing the models' accuracy. We achieve this by using algebraic effects, in order to model sequential effectful programs as instances of the coinductive free monad, that could then be translated into runnable pieces of software by applying the necessary effect handlers. Furthermore, we demonstrate that it is possible to express functional requirements as properties of such models using the first-order modal μ-calculus, a fixed-point dynamic logic which has previously been used to reason about labelled transition systems (e.g. in mCRL2).

This study explores the use of Code Churn and Pattern Size (PSIZ) metrics to identify bug-prone areas in Haskell codebases. The primary research questions addressed are whether these metrics can effectively predict areas of code instability and potential bugs. Our contributions include a comprehensive analysis of these metrics across three large Haskell projects, examining the correlation between high metric values and documented bugs. Our findings reveal that Code Churn is a significant indicator of potential bugs, with ’buggy’ files showing markedly higher mean code churn values. However, the PSIZ metric proved ineffective in predicting bug-prone areas, as the mean and median values for both projects and ’buggy’ files were similar and low. These results suggest that while Code Churn is a useful metric for identifying unstable code areas, PSIZ does not offer the same predictive value. Future research should expand the dataset and consider additional metrics to enhance the reliability of these findings.

The classification of bugs in functional languages is an understudied area, as opposed to imperative counterparts, such as Java. This paper acts as an initial step to cover this gap into two complementary directions. First, a dataset of 142 bugs from 10 Haskell FOSS repositories have been classified according to two taxonomies from literature in order to assess how well they handle the differences in programming paradigms. Based on our bug classifications, the first taxonomy has very little variance in types of bugs, with 86% of bugs being classified in the same category. On the other hand, the second taxonomy showed more potential as the bugs were more balanced between categories, but with occasional difficulties in classification, as some bugs fitted more than one type. Second, we performed interviews with four Haskell developers about their experience with bugs and the usefulness of these taxonomies in practice. They argued that while such taxonomies can prove useful, the context in which it is being used is more important. Thus, circumstances such as the size of the project and team, and stages of development need to be taken in consideration before trying to apply any taxonomy.

The Language Server Protocol (LSP) is a protocol that standardizes the way Integrated Development Environments (IDEs) and text editors communicate with language servers to provide language-specific features like autocompletion, go-to-definition, and diagnostics. While LSP has been widely adopted by mainstream programming languages, its adoption in dependently typed languages has been slower due to the unique challenges posed by their complex type systems and interactive theorem proving capabilities. This thesis explores the potential of LSP for enhancing the development of dependently typed programs, focusing on the Agda programming language. We present the implementation of a prototype LSP server for Agda that leverages scope checking to provide fast and responsive IDE features. We evaluate the performance of the prototype and compare its feature completeness with existing Agda development tools. Our findings demonstrate that scope checking can serve as a foundation for implementing efficient LSP features in Agda, offering a promising direction for improving the tooling and overall development experience for dependently typed languages.

Type-checkers are used to verify certain attributes of programs are correct. Avoiding bugs in type-checkers is especially important when accepting faulty programs has serious real-world consequences. Correct-by-construction programming aims to prevent such bugs by embedding proofs of a program's correctness within the program itself. However, this approach introduces different challenges, such as added complexity. Whether the benefits of correct-by-construction type-checkers outweigh these challenges for more complex language features remains uncertain. This paper investigates correct-by-construction type-checking for a toy language with polymorphic algebraic data types and pattern matching. We do this by implementing a type-checker in the dependently typed language Agda. We show that this approach guarantees a type-checker that does not accept ill-typed terms. Furthermore, we reflect on the challenges of this approach and argue that this approach should be used when a guarantee of correctness is required.

As programming languages become ever more sophisticated, there is growing interest in powerful and expressive type systems. Substructural type systems increase expressiveness by allowing the programmer to reason about the number of times and the order in which variables can be used. This can be used to model different kinds of memory allocation and to construct more expressive interfaces. However, implementing complex type systems requires complex type checkers – this complexity increases the chances of bugs in the type checker itself, which could lead to invalid programs being accepted or valid programs being rejected. The consequences of such bugs can range from programmer frustration to critical errors in production systems.

In this thesis, we develop a correct-by-construction type checker for a toy language with a substructural type system. We use Agda’s dependent type system to intrinsically ensure the soundness and completeness of the type checker. We discuss the advantages and disadvantages of the correct-by-construction approach and find that its complexity likely restricts it to specific use cases.

Typecheckers help avoid bugs in code by catching errors early. Their implementation can, however, be incorrect, leading to inconsistencies in their operation. This research explores how we can use Agda and correct-by-construction programming to create a typechecker guaranteed to be correct in its implementation. For this purpose, I based a toy language on the simply typed lambda calculus extended with records and subtyping. The resulting typechecker is proven to be sound and complete with respect to the typing and subtyping rules of the toy language. This paper compares the correct-by-construction method to existing typecheckers. The new approach offers a greater degree of trust in its implementation but comes at the cost of being more demanding to develop and maintain.

The Correct-by-Construction (CbC) programming paradigm has gained increasing attention, particularly with the rise of dependently typed languages. The CbC approach is often characterized as rigid, rule-based construction process making it suitable for critical infrastructure like type-checkers, which are prone to bugs as they become more complex. However, the specific advantages and disadvantages of using the CbC approach for developing type-checkers in comparison to traditional programming languages remain unclear. Therefore, we investigate the development of a type-checker for a toy programming language extended with checked exceptions using the dependently typed programming language Agda. The results show that the CbC approach, combined with dependently typed languages, is highly effective for the very precise task of type-checker development. Despite the steep learning curve associated with these languages, this method offers notable benefits in ensuring the correctness and reliability of type-checkers. We conclude that this approach is a viable strategy for similar projects in the future.

Various studies already exist about the lifecycle of software programs written in languages like Java, C and C++, but this is an under-reported area for the pure, functional programming language Haskell. This report explores steps in the development of Haskell programs, and particularly, of their bugs. By gaining more knowledge about a bug’s development and its different stages, possible patterns or trends can be found. Using these insights, developers could get a better understanding of the development process, and optimise it. The main question of the research is formulated as ‘What are the different stages of bugs in Haskell programs?’. We consider three different stages: bug introduction, bug detection and bug fixing. To gain more knowledge about these stages, different open-source Haskell repositories, and their bugs were analysed. We found the median time between the bug introduction and detection is 381 days. The median time between the bug detection and fixing turned out to be 3 days. Most bugs were detected and fixed at similar rates regardless of their complexity, except for bugs that were detected by the same developer who introduced the bug. In this case, the time it takes to detect the bug is 30% of the global median. These results motivate developers to check their code more extensively, as they detect bugs quicker than other developers would. It also motivates developers to work with shared code ownership, as having more developers familiar with the code should reduce bug-detection time. Moreover, this study shows that single-statement bugs, which needed a simple fix, occur 2.5 times more often in code when no test is written, which argues for developers to write more test code. Lastly, we recommend repository owners to be more strict with developers working structured and precisely so that they follow Git’s and the repository’s standards and write test code.

Haskell programming language has a long history of extensions which extend and
modify its syntax and semantics. They range from small quality-of-life syntax im-
provements, to complete overhauls of the type system. Such extensions are commonly
implemented directly as a part of Glasgow Haskell Compiler (GHC) or as plugins for
GHC through its plugin API. This paper looks at the present ecosystem of such lan-
guage extensions, identifying the key categories into which extensions can be separated,
based on how often and in which ways they are used, and their functionality.
We analysed which extensions are used in packages uploaded to Hackage, a central
open-source Haskell archive. We further extracted the metadata about the packages,
including the user-submitted tags and maintainer lists, to ascertain how and when are
language extensions used.
The result of our research is a combination of several proposed potential taxonomies,
that can be used by academics and practitioners alike.

When writing functional code that composes multiple recursive functions that operate on a datastrcuture, we often incur a lot of computational overhead allocating memory, only to later read, use, and discard this information.
This can be alleviated using fusion, a technique that combines these multiple recursive datastructure traversals into one.
This thesis explores shortcut fusion using (Co)Church encodings based on the work of Harper (2011), focusing on two questions: What is needed to reliably achieve fusion in Haskell, and the correctness of these transformations through a formalization in Agda.

The first contribution replicates and extends Harper's (Co)Church encodings in Haskell, uncovering optimizer weaknesses and providing practical insights for achieving fusion within Haskell.
The second contribution formalizes these encodings in Agda, leveraging parametricity and the category theory described by Harper.
The formalization proves the equivalence of these encoded functions to the unencoded ones, showing that the encodings are in fact isomorphisms, as long as parametricity (Wadler, 1989) is assumed.

These findings highlight the effectiveness and correctness of shortcut fusion techniques and show the promise of shortcut fusion: Reduce the computational overhead associated with functional programming while retaining its nice, compositional properties.

Static type systems ensure code correctness by aligning implementations with defined type signatures. Despite their benefits in preventing common errors, complex type systems increase the likelihood of bugs within type checkers. Correct-by-Construction (CbC) programming offers a solution by using precise types to create intrinsically verified type checkers, ensuring soundness and potentially completeness. This paper evaluates the use of CbC programming for implementing type inference for the simply typed λ-calculus, focusing on Hindley-Milner (HM) and bidirectional type inference. Implementations in Agda, a dependently typed language, reveal that while CbC programming can eliminate bugs, it introduces significant complexity. HM type inference proves challenging in terms of soundness and completeness, whereas bidirectional type inference is easier to implement but still complex to prove complete. The study highlights the trade-offs of CbC programming, suggesting it is more suited for research and in-depth understanding rather than pragmatic programming.

Dependently-typed languages allow one to guarantee correctness of a program by providing formal proofs. The type checkers of such languages elaborate the user-friendly high-level surface language to a small and fully explicit core language. A lot of trust is put into this elaboration process, even though it is rarely verified. One such elaboration is elaborating dependent pattern matching to the low-level construction of eliminators. This elaboration is done in two steps. First, the function defined by dependent pattern matching is translated into a case tree, which can then be further translated to eliminators. We present a generic, well-typed implementation of this second step in Agda, without the use of metaprogramming and unsafe transformations, by providing a type-safe, correct-by construction, generic definition of case trees and an evaluation function that, given an interpretation of such a case tree and an interpretation of the telescope of function arguments, evaluates the output term of the function using only eliminators. We only allow case splits on variables from a fixed universe of data type descriptions, for which we use techniques like basic analysis and specialization by unification.

Formally verified programs can be embedded in larger non-verified code bases by means of syntactically faithful source-to-source translation: systems like Agda2Hs make it possible to translate verified code written in a dependently typed programming language to a general-purpose functional programming language, Agda and Haskell in this case. Such systems can enable verification for critical functionality while keeping wider ecosystem access and easier to write code for peripheral functionality. However, this interfacing leaves a gap in the formal guarantees of the verified code: preconditions that were only expressible as a dependent type and have thus got erased upon translation might not be met. We present runtime checking these preconditions as a way to close this gap and ensure that computation does not continue on ill-formed input. As an extension to Agda2Hs, we have implemented a solution to automatically insert runtime checks for the preconditions and only make those definitions accessible in the output that are also checkable. The runtime check insertions do not only cover functions, but also data types and non-class records in the form of smart constructors; higher-order erased arguments are supported as well. We make a formal completeness analysis of a simplified version of the checks we generate for well- and ill-typed programs.
In our solution, class instances are not supported for runtime checking due to their different nature, and capabilities for recovering from a failed runtime check are still rudimentary. Despite these limitations, we conclude that a closure of the input precondition verification gap is possible, and that the development time trade-off in comparison to handwriting checks can be worthwhile.

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

Writing software that follows its specification is important for many applications. One approach to guarantee this is formal verification in a dependently-typed programming language. Formal verification in these dependently-typed languages is based on proof writing. Sadly, while proofs are easy to check for computers, writing proofs can be tedious for developers. One particular proof component that currently requires developers attention in many systems, is associative and commutative (AC) reasoning.
We contribute an extension of dependent type-systems to fully automate AC reasoning. This alleviates developers from this task and allows them to concentrate on other proof components. Our approach works by modifying the conversion checker and doesn't compromise soundness or completeness. Furthermore, our approach reuses existing type-checking components, making it easier to implement. We also implemented our theory as an extension of the Agda type-checker. This allowed us to use this implementation to experiment with some example programs.
This thesis can help language designers decide if they want automatic AC reasoning in their language. For language users it can serve as inspiration on how to use such a type-system and finally for researchers we have ideas for future work.

Agda is a language used to write computer-verified proofs. It has a module system that provides namespacing, module parameters and module aliases. These parameters and aliases can be used to write shorter and cleaner proofs. However, the current implementation of the module system has several problems, such as an exponential desugaring of module aliases. This thesis shows how the module system can be changed to address these problems. We have found that we do not need any desugarings during type-checking, but can instead handle module parameters and aliases during signature lookup by making a small change to the scope-checker, completely eliminating any exponential growth problems and unnecessary complexity. This will allow users to make more effective use of the module system, simplifying their proofs. Furthermore, the improvements to the module system will allow future research to fix the problems with Agda's implementation of pretty-printing, records and open public statements.

How convenient would it be to have an AI that relieves us programmers from the burden of coding? Program synthesis is a technique that achieves exactly that: it automatically generates simple programs that meet a given set of examples or adhere to a provided specification. This is often done by enumerating all programs in the search space and returning the first program that satisfies the requirements. However, these algorithms frequently enumerate redundant programs because of symmetries in the search space. We propose a new constraint discovery system that is able to detect these symmetries in a language and systematically generate symmetry-breaking constraints for them. To test these constraints, we implemented a novel, re-usable framework for program synthesis called Herb.jl. The generated constraints are shown to cut down search spaces to less than 25% of the original size and reduce the enumeration time by a factor of 3. Furthermore, this approach is extended to automatically discover semantic specifications without needing an expert. The effectiveness of these specifications is evaluated with an existing specification-based synthesizer, which shows that adding these specifications is an effective way to cut the synthesis time in half for domains where expert-defined specifications are not available. Together, these approaches demonstrate the effectiveness of extracting additional information from a language and applying it during enumeration.