I’ll be talking about how to specify languages type theoretically in Agda, instead of the usual specification in terms of sets of strings. Conal Elliot has demonstrated how to do this for regular languages. We will be taking a look at context-free and perhaps also data-dependent languages. Fixed points are an important technique I use to accomplish this, but encoding them in Agda is difficult. This research is very much work in progress; I will discuss the complications I have encountered and potential solutions.

Jens Palsberg’s first research publication was an OOPSLA ’89 paper, coauthored with William Cook. In that much-cited paper, the authors identify self-reference as a central feature of inheritance, and analyze it using fixed points. They then define both an operational and a denotational semantics of inheritance, and prove them equivalent. Their proof exploits an intermediate semantics, obtained by step-indexing the operational semantics – an early use of the so-called ‘fuel pattern’.

Proof assistants based on dependent types are powerful tools for building certified software. In order to verify programs written in a different language, however, a representation of those programs in the proof assistant is required. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for.

Tools used in software engineering often balance a tradeoff between generality and specificity. The most important tools in software engineering are programming languages, and the most common ones are General-Purpose Languages (GPLs). Because of their generality, GPLs can be used to develop many kinds of software. Domain-Specific Languages (DSLs) are a more specific counterpart; they are programming languages tailored to a specific domain. DSLs are not generally applicable but can be more effective for developing software within their particular domain.

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 truly modular denotational semantics model of WebDSL. We describe obstacles and possible improvements to the chosen framework that can improve the workflow of constructing and maintaining such model. We find the framework to lack lexically scoped effects and other possible improvements to the algebraic effects framework. We discuss the benefits of implementing such denotational model in a dependently typed language and discuss possible improvements to Haskell’s tooling to improve the support of such frameworks. 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 compiler.

Denotational semantics of type theories provide a framework for understanding and reasoning about type theories and the behaviour of programs and proofs. In particular, it is important to study what can and can not be proved within Martin-Löf Type Theory (MLTT) as it is the basis of proof assistants like Agda, Lean and Coq. Many models, including a certain class of comprehension categories, full and split comprehension categories, have been studied for the semantics of dependent type theories. The motivation for this work comes from the fact that not all comprehension categories are full and split, and one expects that type theories more general than MLTT can be interpreted in a comprehension category which is not full and split. In this thesis, we first study how MLTT is interpreted in full split comprehension categories through concrete examples. Next, we investigate type theories that can be interpreted in comprehension cat- egories which are not necessarily full and split. For this, we propose a candidate type theory for the internal language of comprehension categories by extracting a type theory from the semantics given by a general comprehension category which is not full and split. We also give an interpretation of this type theory in every comprehension category.

This thesis investigates the potential of basing a program synthesis system on a dependent 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 implement a prototype of a search algorithm driven by unsolved constraints typically generated during dependent type checking. We encode a range of synthesis problems 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.

This is a practice presentation of my Haskell’24 talk. Abstract:

I will be presenting my next research project on data-dependent grammars. Data-dependent grammars aim to support common practical disambiguation strategies in one unified formalism. However, current implementations of data-dependent grammars are complicated by implementation details. Instead, I will start from a simple model of parsing, namely Brzozowski derivatives, and augment it step by step until we reach data-dependent grammars.

In this talk, we study the theorem by Clairambault and Dybjer saying that there is a biequivalence between locally Cartesian closed categories and Martin-Löf type theories in univalent foundations. More specifically, we give an analogue of this theorem using univalent categories, and we extend it to several classes of toposes.I start with an introduction to univalent categories, and I shall discuss some of the challenges when interpreting Martin-Löf type theory in univalent categories. After that, I will give a short introduction to comprehension categories, and explain why they are a suitable structure for the semantics of type theory in univalent foundations. Finally, I shall explain how univalent categories are used in this proof, and how they simplify the technical details.

In the first part I am going to present the wider context of my research: designing programming languages with equal support for data and codata types. Codata types are known in the proof assistant community because they are a natural choice for modelling coinductive types such as streams. There are other reasons, however, why one might want to have codata types in a programming language: 1) Codata types are important for modelling non-strict data types such as lazy pairs, since codata types naturally model demand-driven computation. 2) Codata types are essential if the language contains linear types or other modalities. The pair type, for example, splits into two different pair types in linear logic, with one of them corresponding to a data type and the other to a codata type. 3) Data and codata types have different extensibility properties which correspond exactly to the expression problem: Data types can easily be extended with new consumers and codata types with new producers, but not vice versa.

In this presentation, we’re taking a look at syntax representations such as De Bruijn indices and HOAS and their type safe variants. We look at conversions between these representations. Finally, we apply what we learn to free monad representations, ending up with a free relative indexed monad.

In this presentation, we’re going to learn the basics of the Julia type system, where some possible places for expansion are and how that ties into property based testing of Julia code.

Information systems store and organize data, and manage business processes concerned with that data. Information systems aim to support operations, management and decision-making in organizations. Web applications are ideal for implementing information systems. Although existing web frameworks provide abstractions for creating web applications, there are three major issues with current web frameworks.

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to automatically prove or disprove correctness of each submission. We achieve robustness by handling recursion using functional induction and by handling auxiliary functions using function call matching. We achieve scalability using a clustering algorithm that leverages the transitivity of equivalence to discover intermediate reference solutions among student submissions. We implement our approach on top of the Stainless verifier, to support equivalence checking of Scala programs. Our results show that our system is capable of proving program correctness, as well as providing counterexamples in case of incorrect implementations, with a high success rate.

Software language design and implementation often involve specifications written in various esoteric meta-languages. Language workbenches generally include support for precise name-based navigation when browsing language specifications locally, but such support is lacking when browsing the same specifications online in code repositories.

Published paper

mophasco.pdf

Ideally we are able to implement refactorings in a language-parametric way. These refactorings can copy, move, or generate code. As part of these implementation, we often need some mechanism to synthesize references to the copied, moved, or created definitions in the program.

Writing correct software is important for many applications. Dependently typed programming languages can be used to eliminate many kinds of bugs through formal proof of correctness. This proof is easy to check for a computer, but hard to write for developers. One particular task that makes writing proofs hard, is the need to reason about associative and commutative (AC) functions.

Computers execute software to do the tasks we expect from them. This software is written by human beings, we call this programming. The most common way to program is by writing text in a programming language. A programming language is very structured so we can be precise, but ultimately these languages are still for humans to read and write. In order to execute the written program, we need to translate it to a list of tiny instruction steps that the hardware of the computer can execute. This translation is also automated with software. The most common forms this software takes is (1) interpreters that execute a program live as they read it, or (2) compilers that translate the entire program for later execution.

AI has slowly (?) made it into the reality of software engineering (SE) and programming language (PL) research and teaching over the last 10-20 years. For example, in research, think of grammar inference and pretty-printing models in PL; think of bug-prediction models and search-based software re-engineering in SE.

There is a longstanding interest in our community in language extension and mechanisms for easily adding (domain-specific) features to programming languages. One notion of extensibility argues that language extensions should be independently developed such that a programmer can pick the ones needed for their task at hand and compose them with a host language. Previously we have developed some ways to ensure that the composition of language and extension specifications leads to deterministic parsers and well-defined attribute grammars to implement the language.

On the occasion of the PhD defence of Jeff Smits, two doctoral committee members are coming from abroad and will give talks: Ralf Lämmel (Koblenz) and Eric Van Wyk (Minnesota).

Plain context-free grammars are often ambiguous. Therefore, many syntax definition formalisms introduce declarative disambiguation rules such as priority (precedence) and associativity that allow the language developer to disambiguate their grammar. In this talk, I will present our ongoing research that answers the question: What are the formal semantics of declarative disambiguation rules?

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 implemen- tation of the module system has several problems, such as an ex- ponential desugaring of module aliases. This paper 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 sig- nature lookup by making a small change to the scope-checker, com- pletely eliminating any exponential growth problems and unnec- essary 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.

Formal verification is a powerful tool for ensuring program correctness but is often hard to learn to use and has not yet spread into the commercial world. This thesis focuses on finding an easy-to-use solution to make formal verification available in popular programming language ecosystems. We propose a solution where users can write code in a formal verification language and then transpile it into a more popular programming language. We use Agda2HS as a case study to determine what challenges users find in using such a tool, improve selected features, and then conduct a user study to evaluate the usability. We find that detailed documentation, support for commonly-used features in the popular programming language, tools to facilitate verification, and user studies are necessary for the success of such a tool.

Lossless compression implementations typically contain two programs, an encoder and a decoder, which are required to be inverse to one another. We observe that a significant class of compression methods, based on asymmetric numeral systems (ANS), have shared structure between the encoder and decoder – the decoder program is the ‘reverse’ of the encoder program – allowing both to be simultaneously specified by a single, reversible function. To exploit this, we have implemented a small reversible language, embedded in Agda, which we call ‘Flipper’ (available at https://github.com/j-towns/flipper). Agda supports formal verification of program properties, and the compiler for our reversible language (which is implemented as an Agda macro), produces not just an encoder/decoder pair of functions but also a proof that they are inverse to one another. Thus users of the language get formal verification ‘for free’. We give a small example use-case of Flipper in this paper, and plan to publish a full compression implementation soon.

In this talk, I will present my ongoing research about modelling access modifiers (typically used for encapsulation in object-oriented languages) using scope graphs. We will discuss the following visibility modifiers

• Public access
• Subclass-only access (protected)
• Package-only access (internal)
• Private access

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.

As Graph Databases grow in popularity, they are used to answer increasingly diverse and complex queries. However, such databases typically have a very limited query language that cannot express arbitrary algorithms. As a result, many users treat the database as a storage layer to export data from and develop algorithms in external tools, wasting computation power and storage space.

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 it- self 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 lan- guage 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.

For the last decade, teams at Oracle relied on the Spoofax language workbench to develop a family of domain-specific languages for graph analytics in research projects and in product development. In this paper, we analyze the requirements for integrating language processors into large-scale graph analytics toolkits and for the development of these language processors as part of a larger product development process. We discuss how Spoofax helps to meet these requirements and point out the need for future improvements.

We present stack graphs, an extension of Visser et al.’s scope graphs framework. Stack graphs power Precise Code Navigation at GitHub, allowing users to navigate name binding references both within and across repositories. Like scope graphs, stack graphs encode the name binding information about a program in a graph structure, in which paths represent valid name bindings. Resolving a reference to its definition is then implemented with a simple path-finding search.

Static type systems can greatly enhance the quality of programs, but implementing a type checker that is both expressive and user-friendly 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 a type system. However, so far Statix has not been used to implement dependent types, which is a class of type systems which require evaluation of terms during type checking. In this paper, we present an implementation 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.

SDF, Stratego and Spoofax provide a platform for development of domain-specific programming languages. On this platform, the WebDSL project started out as a case study in language engineering, and grew into a reliable tool for rapid prototyping and continuous development of web applications. Our team led by Eelco Visser develops and operates several web applications to support academic workflows. EvaTool governs the process of course quality control, importing questionnaire data, and providing lecturers and education directors with a platform to discuss and agree on improvements. WebLab is an online learning management system with a focus on programming education, with support for lab work and digital exams, used by over 40 courses. Conf Researchr is a domain-specific content management system for creating and hosting integrated websites for conferences with multiple co-located events, used by all ACM SIGPLAN and SIGSOFT conferences. MyStudyPlanning is an application for composition of individual study programs by students and verification of those programs by the exam board, used by multiple faculties at the Delft University of Technology. These tools served as practical case studies for applying the research, and ensure the continued development of the underlying platform.

Conferences are great opportunities for sharing research, debating solutions, and networking. For the organizing committee there is a considerable deal of complexity and effort required to provide attendees and organizers with ways to find and manage programs, sessions, papers, tracks, talks, and authors. Eelco Visser found an opportunity to provide an integrated solution to these problems by designing the Conf Researchr conference management system in 2014 using our own domain-specific web programming language WebDSL. In this paper, we highlight the impact Eelco had on conference management, and how Conf Researchr evolved to become the platform of choice for hosting over 900 conference and workshop editions in SIGPLAN and SIGSOFT, among other areas of computer science research.

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.

Substitution is a common and popular approach to implementing name binding in definitional interpreters. A common pitfall of implementing substitution functions is variable capture. The traditional approach to avoiding variable capture is to rename variables. However, traditional renaming makes for an inefficient interpretation strategy. Furthermore, for applications where partially-interpreted terms are user facing it can be confusing if names in uninterpreted parts of the program have been changed. In this paper we explore two techniques for implementing capture avoiding substitution in definitional interpreters to avoid renaming.

Spoofax is a language workbench. A Spoofax language specification generally includes name resolution: the analysis of bindings between definitions and references. When browsing code in the specified language using Spoofax, the bindings appear as hyperlinks, supporting precise name-based code navigation. However, Spoofax cannot be used for browsing code in online repositories.

Compilers transform a human readable source language into machine readable target language. Nanopass compilers simplify this approach by breaking up this transformation into small steps that are more understandable, maintainable, and extensible. We propose a semantics-driven variant of the nanopass compiler architecture exploring the use a effects and handlers to model the intermediate languages and the transformation passes, respectively. Our approach is fully typed and ensures that all cases in the compiler are covered. Additionally, by using an effect system we abstract over the control flow of the intermediate language making the compiler even more flexible. We apply this approach to a minimal compiler from a language with arithmetic and let-bound variables to a string of pretty printed X86 instructions. In the future, we hope to extend this work to compile a larger and more complicated language and we envision a formal verification framework from compilers written in this style.

We present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a tree-based search over a user-specified set of proof rules. It supports safe and unsafe rules and uses a best-first search strategy with customisable prioritisation. Aesop also allows users to register custom normalisation rules and integrates Lean’s simplifier to support equational reasoning. Many details of Aesop’s search procedure are designed to make it a white-box proof automation tactic, meaning that users should be able to easily predict how their rules will be applied, and thus how powerful and fast their Aesop invocations will be. Since we use a best-first search strategy, it is not obvious how to handle metavariables which appear in multiple goals. The most common strategy for dealing with metavariables relies on backtracking and is therefore not suitable for best-first search. We give an algorithm which addresses this issue. The algorithm works with any search strategy, is independent of the underlying logic and makes few assumptions about how rules interact with metavariables. We conjecture that with a fair search strategy, the algorithm is as complete as the given set of rules allows.

During this talk I’ll present a project I’ve been working on during the past month: a Haskell EDSL for writing static-site generators in Haskell. Behind this DSL is actually a full-fletched embedded build system, that should satisfy many properties: incremental, parallel, and self-tracking (hopefully, this is WIP).

Programming Language design is still a rapidly evolving field. There are recent developments in type systems, parallel computing, memory management, etc. However, experimenting with new designs or designing small languages for specific purposes is costly because it requires building a new compiler which currently has few opportunities for reuse.

In reverse language engineering, with its applications to software quality assessment, static analysis, software maintenance and evolution, refactoring, and renovation, the first question is always how to obtain a high-quality parser for the given language(s). During the last two decades, a storm of open-source, open-access, open compiler frameworks for programming languages have shifted the balance from “better generate parser” to “better map an existing parser” completely. Nevertheless important quality considerations (like high-fidelity, low-noise, and efficiency) are still under scrutiny. In this talk we revisit a number of mapped parsers and rewritten grammars for (legacy) programming languages in the Rascal eco-system: Java, C/C++, PHP, Ada; and we discuss implementation effort and design decisions, next to common problems. Recently, it was made possible for Rascal programmers to use also “concrete syntax matching” on syntax trees that were acquired from external sources. This final blow completely unbalances the trade-off towards parser reuse and lets grammers in the corner of the domain-specific languages. Or doesn’t it?

In Fall 2022, I taught an undergraduate course at Johns Hopkins University entitled “Introduction to Proofs” using the Lean Proof Assistant. In this talk, I will report on this teaching experiment.

Dependently-typed languages are attracting more attention in the recent years.

paper: https://arxiv.org/abs/2212.04182

In this talk I will present our recent results on binary translation of concurrent programs from x86 to ARM. More specifically, I will discuss the challenges due to the differences between the x86 and ARM weak memory concurrency models.

In this talk, I will give a demo of a proposed new feature for Agda that was prototyped during the recent Agda meeting in Edinburgh. The PR for this features can be found at https://github.com/agda/agda/pull/6354. After the demo, I’d like to lead a discussion on some remaining design questions.

Computer architectures with weak memory models, such as ARMv8 and ARMv7, allow memory accesses to be reordered in many situations. Fency is a static analysis tool that inserts memory fences to ensure that a program exhibits the same behavior when run on a weaker memory model. We expand Fency with a new dependency tracking analysis, integrate it with LLVM’s alias analysis infrastructure, and improve its usability. (thesis link)

Interaction trees are an active development in representing effectful and impure pro- grams in the Coq proof assistant. Examples of programs they can represent are programs that use: mutable state, concurrency and general recursion. Besides representing these programs we also want to reason about and verify these programs using separation logic. That is the purpose of this thesis. More technically speaking interaction trees are new way to do shallow embeddings in the Coq proof assistant. They are a coinductive variant of the free monad and come with the usual constructions of events and event handlers. The aim of interaction trees is to represent impure programs and potentially non-terminating programs in their environment. Interaction trees are, in contrast to relational operational semantics, executable by interpretation or program extraction. Interaction trees come with a framework for reasoning about their behavior based on equivalency up to weak bisimulation. An open problem is to reason about interaction trees utilizing a separation logic rather than weak bisimulation. We developed Pothos as a solution to this problem. Pothos has an Iris based concurrent separation logic for interaction trees. We address the problem in a non-extensible setting, with mutable state, non-termination and concur- rency as our chosen effects. Pothos inherits all the executable properties from interaction trees and includes a novel relation of Iris’s step-index with coinductive types. We have proven our logic to be sound and include a case study of a spin lock library. The case study shows that our logic is both non-trivial and can utilize the standard Iris patterns for concurrency.

Bisimulation, made popular by Robin Milner, is the primary behavioural equivalence for process equivalence. When there are unobservable actions, often denoted by tau’s, are around, branching bisimulation is a natural equivalence. In this talk I will provide an overview about the efficient algorithms for both that actually match natural lowerbounds. I will quickly do the same for parallel algorithms and end with an intriguing, and as it stands difficult, open question.

This is a SPLASH’22 talk.

This is a SPLASH’22 talk.

This is a SPLASH’22 talk.

This is a SPLASH’22 talk.

This is a SPLASH’22 talk.

Digital printing systems allow for the production of a large variety of different products. Making production plans for all these different products is challenging. One of the challenging aspects of making these production plans is choosing the right sequence of machines, to produce the desired intent. This is challenging due to three aspects: the large number of interdependent variables in the problem instances, the variability of machines, and the search for the best solution from a large set of valid solutions. In this thesis, we implement and evaluate the use of a domain-specific language (DSL) called RSX (Routing Space eXploration), to assist in choosing a sequence of machines. We do this together with an industrial partner. For RSX we use a model-driven approach, and it can be used to model the devices, production steps, and product properties of the digital printing domain. It transforms those into a constraint model described in the MiniZinc language, which is used as input for a constraint solver. We present the implementation of the RSX language and MiniZinc constraint model, and we evaluate the language coverage, accuracy, and performance. From these evaluations, we conclude that RSX can be used to model a number of cases, which were characteristic in the context of our industrial partner. Furthermore, we conclude that RSX can compile and solve the evaluated cases in the order of a few seconds and that the implementation is accurate, such that it can be used as a proof of concept.

In this thesis, we have defined a symbolic execution technique to automatically generate test suites for programs written in functional programming languages that can find the behavioural differences between a reference implementation and a set of potentially different implementations. Our symbolic execution technique uses a constraint solver in order to find a model that satisfies all constraints that together represent an execution path through the program. Furthermore, our technique utilises manually defined budget constraints to guide the symbolic execution to more interesting areas of the programs. These budget constraints define an initial budget that dictates when the symbolic execution terminates, and a set of costs associated to certain operations such as calling (specific) functions or performing (specific) pattern matches. This allows the symbolic execution to deplete budgets faster when it explores functions or branches of a program that are deemed “unlikely to be interesting”. This results in less system resources being used on exploring these uninteresting execution paths, and instead allows for exploration of deeper paths in more interesting areas of the programs. Our budget constraint optimisation strategy works alongside other well-known optimisation strategies for symbolic execution such as early branch pruning and reusing intermediate results, more commonly known in the field of symbolic execution as compositioning.

In this seminar, I present my progress on developing a modular approach to definitions of dynamic semantics and in particular compilation. Using higher-order effects we can describe components of our source language as abstract monadic operations. These abstract operations can be given a semantics individually in terms of lower level operations. We can repeat this process many times until we are finally left with only operations that correspond directly to, for example, X86 assembly instructions.

In this thesis, we develop a new library for Agda named Attic, which allows us to create and compose proof tactics that can be used to generate terms through reflection. Such tactics can be converted to Agda macros, allowing them to be used in term positions where they can generate term solutions of the expected type. Tactics can make the development of proofs faster by making proofs easier to read and write. This project can be seen as a sister project to Ataca, which is an earlier attempt at developing tactics that operate through reflection. Attic explores new mechanisms of operation, such as non-determinism with iterators to allow for multiple solutions, and the use of deferred unification, so that the final proof term is only fully constructed at the end of tactic evaluation. To allow for the representation of both finite and infinite sequences that can be consumed step-by-step, we have implemented the iterator data type in Agda. Although iterators existed in other systems previously, an Agda implementation had not been made. These iterators underpin the branching mechanism in tactic instructions, and support operations that can be used to generate, transform and filter values. Finally, we have implemented a number of tactics and operations that are commonly found in other proof assistants. We also compare the resulting library to the Ataca library and examine the differences in runtime for a small test case. While Attic is not yet a complete solution, we present new ideas that may be incorporated in future tactic systems.

There are a few established implementations of dependently-typed languages like Agda, Coq or Idris. However successful they are the implementation details are quite complex and only a few dare to extend them. This exists in contrast with Haskell, which has a rich culture of extensions, both in the form of pragmas and plugins.

The dynamic semantics of a programming language formally describe the runtime behavior of any given program. In this thesis, we present Dynamix, a meta-language for dynamic semantics. By writing a specification for a language in Dynamix, a compiler for the language can be derived automatically.

Formal verification of imperative programs can be carried out on paper by annotating programs to obtain an outline of a proof. This process has been mechanized by the introduction of separation logic and computer assisted verification tools. However, the tools fail to achieve the readability and convenience of manual paper proof outlines. This is a pity, because getting ideas and proofs across is essential for scientific research. We introduce a mechanization for proof outlines of imperative programs to interactively write human readable outlines in the dependently typed programming language and proof assistant Agda. We achieve this by introducing practical syntax and proof automation to write concise proof outlines for a simple imperative programming language based on λ-calculus. The proposed solution results in proof outlines that combine the readability of paper proof outlines and the precision of mechanization.

Build systems speed up builds by reusing build step outputs from previous builds when possible. This requires precise definitions of the dependencies for build steps. Pipelines for Interactive Environments (PIE) is a build system with precise dependencies, but its task definitions in Java are verbose. The PIE Domain Specific Language (DSL) allows pipeline developers to write concise definitions of PIE tasks, but the PIE framework has evolved and the PIE DSL cannot express many tasks and projects.

Dataflow analysis is a powerful tool used for program optimization, static analysis, and editor services for many programming languages. Spoofax, a language workbench, contains a domain-specific language called FlowSpec for the definition of control-flow and dataflow semantics that language developers can use to implement dataflow analyses for their language. FlowSpec however cannot be used to efficiently optimize programs. Other solutions are not suitable for language developers, or lack the ergonomics of a domain-specific language. In this thesis we present Flock: an incremental implementation of FlowSpec. We analyze the performance of Flock and show that it is efficient enough for use in optimization pipelines. Flock gives language developers the tools to succintly write dataflow analyses for a wide variety of applications.

Refactorings are program transformations that preserve the observable behavior of the program. The refactoring function inlining replaces a function call with the contents of the referenced function definition. To preserve the behavior, properties such as reference relations must be retained and language constructs like ‘return’ statements must be replaced. Implementing a behavior preserving refactoring is a time-consuming and error-prone task. In the past, such refactorings have only been implemented for one language at a time, thus they can not be reused in other languages.

Inductive data types have become an important tool in functional programming and in particular in the design of programming languages as they are used to define the type of terms in the sought language. Initial Algebra Semantics characterizes the set of terms, using the framework of Category Theory, as initial objects in specific categories, those of F-algebras. In this talk, we first introduce the necessairy background of Category Theory. Then, we work our way up to the general framework of F-algebras guided by examples.

In this talk I’ll start by presenting the logical framework Dedukti, a language which allows for the definition of various logics and systems, and its applications for rechecking and sharing proofs. I’ll then discuss my research project, which concerns the encoding of type theories in Dedukti. One of the main practical applications of this work is the development of the Agda2Dk translator, allowing to translate Agda proofs into their representation in Dedukti.

Web APIs are being used for increasingly larger and complex use cases. Right now it can be hard to make sure that what is documented about an API is correct everywhere and to know if a change will have impact on the users of a web API. When details are missing in an API specification users of that API need to make assumptions about how the API works. The creators of the web API also wants to know what users expect from the API. There are two sides to this problem, enforcing that the implementation is actually the same as what is specified, and making it possible to define API specifications as precise as possible.

Intrinsically-typed interpreters are an attractive approach for verifying type safety: one specifies the operational semantics of the object language by writing an interpreter in a dependently-typed host language, and type checker verifies that this semantics is type safe. This approach, however, relies on (indexed) data types and pattern matching functions, which require the entirety of a language’s syntax and semantics to be defined at once. Consequently, we cannot reuse (parts of) a specification without copying or re-typechecking existing code. In this talk, we discuss how to define language fragments that are both intrinsically typed and intrinsically composable. Such language fragments form a self-contained partial specification of language’s syntax and semantics that is safe by construction and composable by design. Additionally, language fragments are closed under a composition operation that preserves safety and composability, allowing for type safe language specifications to be assembled by composing multiple fragments.

Despite the popular opinion of artificial intelligence being centred around deep neural networks and numerical representations, several of its subfields exploit programming languages as an abstraction for solving complex tasks. In this talk, I will give a short introduction to two such research areas, program synthesis and probabilistic programming, introduce some of the challenges and outline potential connections for the programming languages community.

Pattern matching is the act of checking if a value is in the set of values described by a pattern. Many programming languages provide constructs to pattern match on program values. Pattern matching constructs appear in different variants. Stratego, a term rewriting language, features first-class pattern matching, which attempts to match a pattern with a value. If the match is successful, variables in the pattern are bound. If the pattern does not match, the matching expression fails. Using choice and sequence operators, one can build expressions that attempt to match multiple patterns matches until one succeeds, evaluating the expression that corresponds to that pattern. This is a common way of branching in Stratego programs. The Stratego compiler handles each match attempt independently, disregarding the context.

Type-checking is of vital importance to program robustness. In addition, type information can be used in program transformation/optimization, improving performance, and for editor services, improving the productivity of a programmer.

In languages like Haskell or Ocaml, where programmers are encouraged to introduced new datatypes at will to suit the problem at hand, some machinery is made available in the language itself to relieve users of the burden of reimplementing basic constructions again and again. With such a deriving mechanism, users can retrieve things like decidable equality for free. In Agda however, such a practical system is not available as is. Reflection is powerful and can get you quite far, but it’s complex, tedious, and uses an untyped representation of terms.

This talk presents a tool for genetic program repair utilizing the rich features provided by Haskell and the available frameworks. It covers basics of program repair, genetic search and typed holes. We then look at our novel approach of type-based program repair using properties and present some of the (mixed) results we achieved. In general, the patches are cool but often too fine-grained, but we hope that they can help especially for classroom settings. The program and a sneak-preview can be found on github https://github.com/Tritlo/Endemic

Many incremental type-checkers use standardized techniques to achieve incrementality, such as tracking dependencies between compilation units and identifying module interfaces, which are all declarations in a module that are visible externally.

In ongoing work, we have been developing a meta language (working title Strachey) for defining and composing programming language components. One of the key challenges of designing a type system for this language is to retain static type safety of pattern matching definitions in light of future extensions of data types with new constructors. In this talk, I discuss recent experiments on developing a calculus with row types in which we can encode (and type) extensible functions over extensible data types. Eventually, the goal is to use this calculus as a core language for Strachey, providing a well-understood and principled foundation for the surface language. I will also discuss some of the remaining challenges, such as encoding row-typed effects, and providing decent error reporting when type checking Strachey by going through a core language.

The PhD thesis is about the design of meta-languages for the specification and implementation of typed programming languages, such that the implementation is formally proven type-correct. For language front-ends—i.e., type checkers—the thesis contributions a method for automatically obtaining sound type checkers from declarative type-system specifications. Language back-ends—i.e., interpreters and compilers—are developed in the dependently typed meta-language Agda in an intrinsically typed style so that the implementation also encompasses a type-safety proof. The contributions of the thesis there is to make it to scale these ideas from simply typed functional languages, to languages with references a la ML or concurrency and session-typed cross-thread communication, and a low-level language with labels and jumps. This is made possible by developing, among other things, an abstract, shallowly embedded separation logic in Agda, as a basis for functional abstractions (e.g., monads) that encapsulate both computational work and proof work.

The goal of the Agda Core project is to ensure the trustworthiness of Agda by means of a small core language that is deeply embedded in Agda itself. I also intend to explore its potential as the basis for meta-programming and proof exchange with other languages. As the first step in the development of Agda Core, I am currently focusing on defining the syntax of Agda Core. In this seminar I would like to discuss the crucial question of how to represent variables, scopes, and binding structure of this syntax.

Robustness of a concurrent program ensures that its behaviors on a weak concurrency model are indistinguishable from those on a stronger model. Enforcing robustness is particularly useful when porting or migrating applications between architectures. Existing tools mostly focus on ensuring sequential consistency (SC) robustness which is a stronger condition and may result in unnecessary fences.

Developing and exporing new programming languages requires significant effort and expertise on behalf of language designers. For this reason, it is an ongoing topic of research in the PL community to enable the development of languages by composing and reusing pre-defined definitional interpreters for language features. In this talk, I’ll describe some of the main challenges with defining composable interpreters, and describe our recent efforts on developing a new language with integrated support for defining and composing interpreters.

The Scannerless Generalized LR (SGLR) parsing algorithm supports the development of composed languages seamlessly but does not support incremental parsing. The Incremental Generalized LR (IGLR) parsing algorithm, on the other hand, does not support the seamless composition of languages. This thesis presents the Incremental Scannerless Generalized LR (ISGLR) parsing algorithm and investigates the effects of combining the SGLR and IGLR parsing algorithms. While the algorithmic differences are orthogonal, the fact that scannerless parsing relies on non-deterministic parsing for disambiguation has a negative impact on incrementality. Nonetheless, we show that the ISGLR parsing algorithm performs better than the batch SGLR parsing algorithm in typical scenarios. On average, the ISGLR parser can reuse 99% of a previous parse result. When parsing from scratch, the ISGLR parser has a 24% run time overhead compared to the SGLR parser, but when parsing incrementally for changes that are smaller than 1% of the input size on average, it has a 9× speedup.

Software systems are trusted with a wealth of sensitive data. They are so complex and hard to get right that opportunities for attacks abound, ranging from application bugs to leaky runtime systems, and even hardware security vulnerabilities. How can we ensure that our data is really secure in our systems?

Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. In this talk I will present a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.

Incremental analysis is of indispensable value for software engineers. They allow for real-time editor feedback, and minimal build times, even for larger projects in languages with complicated type-systems. In this talk, I will tell about my current research in providing implicit incrementality for type-checkers that use the scope graph theory for name resolution. This incrementality is based on two core ideas. First, we want to validate whether answers to queries from the previous result have changed, based on difference in the scope graphs. When answers are stable, we don’t need to restart the type-checker for a compilation unit, but instead we can reuse the result. Second, since this framework executes type-checkers concurrently, special attention to deadlock should be payed. Particularly, when the deadlock only contains unstarted units, we can immediately reuse all of their results, which saves a lot of computation time. Otherwise, we restart all currently unstarted units. In this way, we want to create reasonable execution times for Statix type-checkers, even for larger projects and specifications.

Agda2Hs https://github.com/agda/agda2hs is a new backend for Agda that translates a subset of Agda to readable Haskell code. The main goal of this project is to write and verify code in Agda that can be integrated seamlessly into Haskell projects. In this talk I will report on the work done by five undergraduate students at TU Delft to port five Haskell libraries (Data.Map and Data.Sequence from the containers package, Data.Graph.Inductive from the fgl package, and the QuadTree and Ranged-sets packages) to Agda, verify their pre- and post-conditions and internal invariants, and translate the verified implementations back to Haskell using Agda2Hs.

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. However, correctly implementing refactorings is notoriously complex, and these state-of-the-art implementations are known to be faulty and too restrictive. Rename is the most-commonly applied refactoring and is used to change the identifier of a language entity such as a variable, a function or a type. Spoofax is a language workbench that allows language engineers to define languages through declarative specifications. When developing a new programming language, it is both difficult and time-consuming to implement automated refactoring transformations. Therefore having an out-of-the-box Rename refactoring would be of great help, as new languages often lack such tool support. We developed a sound language-parametric Rename refactoring algorithm that works on an abstract model of a program’s name binding structure. We implemented that algorithm in Spoofax, using the Stratego transformation language. We successfully tested the algorithm on five different languages implemented in Spoofax, which use both NaBL2 and Statix to declare their static semantics and name binding rules. As a result, Spoofax now offers language engineers an automated Rename refactoring that works for whatever language they might develop.

Compilers translate high-level source code into low-level machine code. To represent source code a compiler uses a language called the intermediate representation. An intermediate representation for the compilation of functional languages is continuation-passing style [21, 2]. It provides convenient abstractions for both data flow and control flow.

In this lunch talk, I will discuss the design of my (online) professional education course that is intended to teach people with a background in CS some new skills that they can apply in their daily jobs. Concretely, this course teaches the fundamentals of functional programming who so far mostly only experienced imperative programming styles, connects this with the systems aspects of running code on clusters of machines from a distributed systems point of view, and then introduces the learners to commonly used big data processing systems and how a more functional programming style makes programs more scalable. I can report my experiences working with the Extension School on the course development and implementation and how the first edition of the course turned out last fall. We are scheduled for a re-run in late April and are preparing a few of structural changes based on the lessons learned.

Context-free grammars (CFGs) provide a well-known formalism for the specification of programming languages. They describe the structure of a program in terms of parse trees. One major issue of CFGs is ambiguity, where one sentence can sometimes have multiple different parse trees. Some formalisms like SDF3 allow annotating a grammar with disambiguation rules, such as priority or associativity rules. Disambiguation rules filter out certain invalid parse trees, making a grammar less ambiguous.

This thesis introduces the FrameVM virtual machine and the Framed language. This language gives developers a target to compile to which concisely follows the scopes-as-frames model. This model allows language developers to derive the memory model based on the scope graphs. The core building blocks of Framed are frames, which contain all data including code. To demonstrate the viability of this model this paper also introduces a compiler from Scheme to Framed, focussing on complex control structures such as call-with-current-continuation and closures. As a result we aim to show that Framed is usable as a target language for compiling, even though it does not have a stack nor registers.

Large scale production distributed systems are difficult to design and test. Correctness must be ensured when processes run asynchronously, at arbitrary rates relative to each other, and in the presence of failures, e.g., process crashes or message losses. These conditions create a huge space of executions that is difficult to explore in a principled way. Current testing techniques focus on systematic or randomized exploration of all executions of an implementation while treating the implemented algorithms as black boxes. On the other hand, proofs of correctness of many of the underlying algorithms often exploit semantic properties that reduce reasoning about correctness to a subset of behaviors. For example, the communication-closure property, used in many proofs of distributed consensus algorithms, shows that every asynchronous execution of the algorithm is equivalent to a lossy synchronous execution, thus reducing the burden of proof to only that subset. In a lossy synchronous execution, processes execute in lock-step rounds, and messages are either received in the same round or lost forever—such executions form a small subset of all asynchronous ones. We formulate the communication-closure hypothesis, which states that bugs in implementations of distributed consensus algorithms will already manifest in lossy synchronous executions and present a testing algorithm based on this hypothesis. We prioritize the search space based on a bound on the number of failures in the execution and the rate at which these failures are recovered. We show that a random testing algorithm based on sampling lossy synchronous executions can empirically find a number of bugs—including previously unknown ones—in production distributed systems such as Zookeeper, Cassandra, and Ratis, and also produce more understandable bug traces.

Programmers in Racket gradually learn to create domain-specific languages, first via macros that serve as simple syntactic abstractions, and later as libraries of macros that work together to create complete DSLs. Racket’s macro technology smooths the way via expressive syntax matching and templating, automatic name hygiene, and safe separate compilation. However, conventional macros are limited: DSLs with static semantics and optimizing compilers remain difficult to implement and integrate with the host language. This talk describes our work on new tools to support these features. First, an architecture and reflective API for building extensible DSLs that macro-expand to a DSL core language, enabling traditional compilation techniques. Second, a work-in-progress design for a declarative meta-language to allow Racket programmers to create sophisticated DSLs without deep knowledge of the macro system.

Modules are, in one form or another, present in almost all programming languages. ML languages famously provide an extremely rich module system that form a second language designed to provide large-scale composition and abstraction. The principal mainstream represent of this tradition is the OCaml language. In this talk, I’ll present ML modules in practice, through OCaml examples and live-coding, and in theory, with a presentation of the underlying theory, and the sort of meta-theoretical guarantees we can expect. We will then take a quick tour of the “new cool kids”, promising alternative formulations of modules such as 1ML, and what feature they bring.

Abstract interpretation is a way of approximating the semantics of a computer program, in which we derive properties of those programs without actually performing the necessary computations for running the program, though the use of an abstract interpreter. To be able to trust the result of the abstract interpretation, we would to able to prove the soundness of the approximations of the interpreter. Previous work by Keidel et al. has shown that the soundness proofs of an entire abstract interpreter can be simplified by decomposing the interpreter by implementing concrete and abstract interpreters as instantiations of a generic interpreter. The goal of this thesis is to explore and implement mechanical proofs of soundness of such interpreters. To this end, we have used the interactive proof assistant Coq to implement a generic interpeter for a simple imperative language and instantiate it both concrete and abstract versions. The abstract interpreter is automatically proven sound via the use of Coq’s automatic proof capabilities and typeclass system. Both the interpreted language and the used abstractions can be expanded to allow for more features. Soundness proofs can then be written for just the new components, those proofs will then be automatically resolved by Coq.

Static Analysis is of indispensable value for the robustness of software systems and the efficiency of developers. Moreover, many modern-day software systems are composed of interacting subsystems developed using different programming languages. However, in most cases no static validation of these interactions is applied.

Intrinsically-typed definitional interpreters are an attractive way to define languages, tightly integrating specification and proof. Although is is common to define the same constructs for different languages, copy-paste reuse is still the de-facto standard way of sharing code between such interpreters. A preferable approach would be to compose interpreters from separately-defined components.

A lot of programming languages sacrifice safety for the sake of performance and usability. For example, C offers great performance, Python is very easy to use, but neither of the languages provide a way to verify that division by zero or out-of-bound array indexing does not occur in the given program. Extending languages with such safety guarantees tends to require very invasive changes of the tooling and/or language semantics.

Probabilistic programming languages allow programmers to write down conditional probability distributions that represent statistical and machine learning models as programs that use observe statements. These programs are run by accumulating likelihood at each observe statement, and using the likelihood to steer random choices and weigh results with inference algorithms such as importance sampling or MCMC. We argue that naive likelihood accumulation does not give desirable semantics and leads to paradoxes when an observe statement is used to condition on a measure-zero event, particularly when the observe statement is executed conditionally on random data. We show that the paradoxes disappear if we explicitly model measure-zero events as a limit of positive measure events, and that we can execute these type of probabilistic programs by accumulating infinitesimal probabilities rather than probability densities. Our extension improves probabilistic programming languages as an executable notation for probability distributions by making it more well-behaved and more expressive, by allowing the programmer to be explicit about which limit is intended when conditioning on an event of measure zero.

We consider how to use modular effects to define modular languages with lambda abstraction. We argue that existing approaches to algebraic effects and handlers are not suitable for this challenge. Instead, we propose a new approach that we dub staged effects and handlers. We show how to use our approach to define lambda abstraction in a modular way, and discuss open questions.

A Guarded Kleene Algebra with Tests (GKAT) is a type of Kleene Algebra with Tests (KAT) that arises by restricting the operators of KAT to “deterministic” (predicate-guarded) versions. This makes GKAT especially suited to reason about flow control in imperative programs. In contrast with KAT, where the equivalence problem is PSPACE-complete, we show that equivalence in GKAT can be decided in almost linear time. We also provide a full Kleene theorem and prove completeness w.r.t. a Salomaa-style axiomatization, both of which require us to develop a coalgebraic theory of GKAT.

In this talk, I will present my work on formally defining a good concurrency model for C/C++ and proving that it satisfies both requirements. Unlike the prior state-of-the-art models, our model is easy to adapt and we have extended it to cover the full range of C/C++ features. I will conclude with a summary of my ongoing work and future research plans.

Speculative execution attacks, such as Spectre, present an enormous security threat, capable of reading arbitrary program data under malicious speculation and later exfiltrating that data over microarchitectural covert channels. This talk will present Speculative Taint Tracking (STT), a comprehensive hardware protection from speculative execution attacks. STT is based on the observation that it is safe to execute and selectively forward the results of speculative instructions that read secrets as long as the STT protection can ensure that the forwarded results do not reach potential covert channels. For performance, STT efficiently disables protection on previously protected data, as soon as doing so is safe. In the talk, we will discuss the security guarantees that STT provides, i.e., enforcement of a novel notion of non-interference appropriate for speculative execution attacks.

Software has integrated deeply into modern society, not only for small conveniences but also for safety-critical tasks. To cope with the ever-increasing complexity of software systems, tools and techniques are needed that support software developers to fully comprehend the behaviours of the systems they develop. In order for such tools and techniques to be truly impactful in real-world scenarios, it is important that they are applicable during the software development process, by the software developers themselves.

Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this talk we discuss how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in quantum programming. We also show our denotational interpretation is invariant with respect to big-step reduction, thereby establishing another novel result for quantum programming. Compared to classical programming, this property is considerably more difficult to prove and we demonstrate its usefulness by showing how it immediately implies computational adequacy at all types. To further cement our results, our semantics is entirely based on a physically natural model of von Neumann algebras, which are mathematical structures used by physicists to study quantum mechanics. Joint work with Romain Péchoux, Simon Perdrix and Mathys Rennela.

The programming languages we use influence how we think about programming and the sorts of programs we write. Thus, it is essential that languages allow programmers to express programs in natural ways that match the programmer’s intention and capture the essence of a task without being cluttered by trivialities that the computer can determine for itself.

In the 13 years since the original release of Agda 2, the module system designed by Ulf Norell has proven itself to be powerful and robust for many applications. However, two pain points in the current implementation are the printing of names coming from imported modules, and the efficiency issues (e.g. https://github.com/agda/agda/issues/4331) arising from the need to copy modules on application.

Writing and extending plugins for Coq in OCaml without extensive familiarity with Coq internals is a challenging task. Fortunately, MetaCoq not only facilitates such tasks, but also provides means for proving correctness of the written plugins. I worked on a plugin that implements subterm relations from the Equations package for Coq. It turned out that while writing the plugin is indeed made simpler by the MetaCoq machinery, there’s still room for improvement in the realm of proofs. I’m also going to talk about other examples of plugins that have been written in MetaCoq and how my experience compares to those cases.

Session types—a family of type systems for message-passing concurrency—have been subject to many extensions where each extension comes with a separate type safety proof. These extensions cannot be readily combined, and existing type safety proofs are generally not machine-checked, making their correctness less trustworthy. We overcome these shortcomings with a semantic approach to binary asynchronous affine session types using a logical relations model in the Iris framework in Coq. We demonstrate the power of our approach by combining various forms of polymorphism and recursion, asynchronous subtyping, unique and shared references, and locks/mutexes, with little proof effort. As an additional benefit of the semantic approach we demonstrate how to integrate manual verification of racy but safe programs as part of well-typed programs.

I will present some work-in-progress on recasting the Statix language more closely in the standard mold of a substructural, or resource, logic. The goal, as for Statix, is to obtain a framework for declaratively specifying static semantics of programming languages using the scope graph model, but one in which we might more easily obtain (complete) descision procedures for satisfiability, model checking/construction, etc. Key features of the approach include allowing “floating” edges in scope graphs, as well as taking only a basic reachability predicate as primitive and deriving more complex notions of query. I will describe how to specify Simply Typed Lambda Calculus using Scope Logic, and then extend this to the Hindley-Milner (ML) type system. I will highlight a general schema: specifications are split into a “spatial” part that describes only the local structure of an underlying scope graph, and a “pure” assertion over this graph that specifies constraints on the data it contains and reachability within it. The background for this work is the “Scopes As Types” paper, and the “Knowing When To Ask” manuscript.

A discussion about what people in the group do for time management.

Over the years virtual machines (VMs) have been created to abstract over computer hardware. This simplified code generation and allowed for easy portability between hardware platforms. These VMs are however highly tailored to a particular runtime model. This improves the execution speed, but places restrictions on the types of languages that the VM supports. In this thesis the Frame VM was developed as a VM that supports many different types of languages in a principled way. Achieving this is done by basing the VM on language independent models of memory and control flow. Usage of the scopes-as-frames paradigm and control frames resulted in an instruction set that is relatively small at its core, but does allow for the construction of complex control flow. As an effect, many different programming languages can be compiled to the Frame VM. In addition to this VM, a Domain Specific Language (DSL) for executable semantics of programming languages was created. This language, Dynamix, allows for a modular approach to writing the semantics of a language. Additionally, Dynamix provides a meta-compiler that uses these semantics of a language to compile programs to the Frame VM. To validate the Frame VM, direct compilers for Rust and Prolog have been created in a student project and compilers for Scheme and Tiger were created using Dynamix. Using these semantics of Scheme and Tiger, it was possible to execute programs containing usage of call/cc and a suite of Tiger benchmark programs. Furthermore, the control flow of Tiger was extended with exceptions and generator functions. This extension did not require any changes to the existing semantics, showing the modularity of control achieved when using Dynamix and the Frame VM.

Associativity and priority rules provide a mechanism for disambiguation of context-free grammars that is based on concepts familiar to programmers from high-school mathematics. However, there is no standardized and declarative semantics for such rules, in particular for the disambiguation of the more complex expression grammars encountered in programming languages.

Creating software for manufacturing systems involves an interplay between mechanics, embedded software, and control software. Validating such software is costly because iterations require work from the different disciplines. The software is also complex, because the systems are parametric and we are interested in maximizing performance or minimizing resource waste. I’ve been working on a domain-specific language for specifying parametric manufacturing systems. With this DSL, we try to improve the software engineering process on two dimensions. First, the DSL introduces early validation by enabling mechanical engineers to carry out validation on the software specification level. Second, the DSL supports global optimization by generating constraint models for which optimal solutions are translated back to the specification level. In this talk I’ll present the DSL, the language engineering techniques behind it, and I’ll discuss my plans for evaluating the DSL within the context of Canon Production Printing. At Canon we have filed a patent for the application of this work to the printing domain. Therefore, I cannot talk about the application to printing, but I will talk about the generic language engineering approach and its application to an alternative, artificial, domain.

We demonstrate how the Iris framework for concurrent separation logic can be used to prove type soundness of feature-rich, realistic languages, using the “semantic approach’’ to type soundness. Contrary to the traditional “syntactic approach” of progress and preservation, the semantic approach has several advantages in terms of reasoning about data abstraction and unsafe features. We show that the semantic approach leads to clear and concise proofs that can be effectively mechanized using the implementation of Iris in the Coq proof assistant. This is joint work with Amin Timany, Derek Dreyer, and Lars Birkedal.

I’ve been working on using the framework that we developed for intrinsically typed interpretation of linear language (CPP ‘20) to get compositional typesafe compilation of an imperative language. The key idea being that we can model label binding in JVM bytecode using these ‘proof relevant separation algebras’ that also powered our previous work. In this demo I hope to give you an idea of how this works and I hope to gain some insight into how I may explain it on paper.

Stratego is a term transformation language that inspired many a functional programming library for “generic programming”: generic traversal over data. Most of these libraries have the downside that they are all more limited in expressive power, because they work on typed tree representations. In Stratego, we can write arbitrary rewrite strategies that define the traversal over data, because Stratego is more dynamically typed. The upside of having typed trees though, is that you can quickly catch typing mistakes. Bugs in Stratego code can be a pain to debug, especially in situations with backtracking.

Incremental type checking is essential for a good developer experience in large software projects. The goal of incremental type checking is to reduce the amount of work that is redone when only some of the files in a project change. Making a type checker incremental from a regular type checker is a non-trivial task. Approaches for incremental type checking go back to at least the early 1980s. However, general approaches lack support for more advanced features such as dependency discovery and mutually recursive dependencies. These advanced features are only found in approaches for specific languages. In this talk I present a language-agnostic approach to incremental type checking that supports dependency discovery and mutually recursive dependencies. The approach requires the type checker to use scope graphs for name binding and resolution, but otherwise puts few requirements on the type checker’s internals.

Using dependent types we can provide a comprehensive specification for many programming languages by writing a definitional interpreter, encoding the static semantics as invariants over our abstract syntax type. The benefit of this approach is that the semantics of the host language guarantees certain poperties we might care about, such as type soundness. The downside, however, is that these interpreters are monolithic in nature, and thus less practical for larger languages. We investigate how and when these definitional interpreters can be composed, drawing inspiration from existing solutions in the design space surrounding the expression problem.

High-tech industrial systems rely more and more on embedded software for their key differentiating features. Embedded software is often reused for multiple product generations, and evolves through regular maintenance and feature extensions. However, this evolution increases the size and complexity of the software, and forms a challenge for further product innovation.

Univalent Parametricity is a new heterogenous extension of parametricity strengthened with univalence. It makes it possible to prove & program modulo equivalences, and transfer definitions and theorems between equivalent types as if they were equal. This allows one to easily switch between representations that are easy to reason about and computationally-efficient representations, seamlessly. We will see how univalence & parametricity alone cannot transfer proofs as one would hope, and how it is made possible with univalent parametricity. Then I will talk about the current implementation of Univalent Parametricity in Coq, and the WIP re-implementation I’ve been doing using MetaCoq, a framework which allows metaprogramming in Coq (among other things).

Dependently typed languages provide strong guarantees of correctness for our programs and proofs, but they can be hard to use and extend. To increase their practicability and expressivity, they can be extended with user-defined rewrite rules. However, this is dangerous as it is very easy to break expected good properties of these systems, e.g., termination, confluence, canonicity or subject reduction [3]. Among those, confluence is a key ingredient to retain subject reduction and as such is essential.

Questions that we can discuss:

• How to approach a new topic? Where to start reading?
• How does one delimit the scope of related work? How to prevent it becoming a time sink?
• Why is related work important?
• When do you research related work?
• What are your responsibilities as a master student/phd student/paper author?
• How to make effective use of related work? When is it worth trying to use an existing formalism rather than designing something new?
• How to write a good related work section? Where does it go in a paper?
• Should I discuss related work in a talk? If so, how?

The Spoofax Testing Language (SPT) is the existing solution for testing in the Spoofax language workbench. It allows developers of domain specific languages to write their test cases declaratively. As it aims to be implementation agnostic, developers don’t need to concern themselves with the details of the artifacts generated by Spoofax, and can write their tests before implementing their language. However, the previous implementation has become slow and unusable for larger test suites and can not be executed programatically. This means it can’t be used for continuous integration and automated regression testing. As Spoofax was redesigned to become more robust and platform independent, the previous SPT is no longer compatible. We took this opportunity to redesign SPT.

In this informal chat we will discuss how to cite the scientific literature. We will discuss the various kinds of publications, how they correspond to the various kinds of entries in BibTeX, and why it is important to cite correctly. And I will advocate the use of researchr (and give a demo) to collect high quality, reusable bibliographies for your papers. (It will be an informal chat since I will prepare minimally for the event and rely on your questions and other forms of audience participation.)

We present an abstract, set-theoretic denotational semantics for a significant subset of OCaml and its module system, allowing to reason about the correctness of renaming value bindings. Our semantics captures information about the binding structure of programs, as well as about which declarations are related by the use of different language constructs (e.g. functors, module types and module constraints). Correct renamings are precisely those that preserve this structure. We show that our abstract semantics is sound with respect to a (domain-theoretic) denotational model of the operational behaviour of programs, and that it allows us to prove various high-level, intuitive properties of renamings. This formal framework has been implemented in a prototype refactoring tool for OCaml that performs renaming.

An intrinsically-typed definitional interpreter is an attractive way of specifying the dynamic semantics of a programming language. It is a concise specification that is executable and type safe by construction. Unfortunately, scaling up intrinsically-typed definitional interpreters to more complicated object languages often results in definitions that are cluttered with manual proof work. In linearly-typed languages (e.g., session-typed languages) one has to ensure that all values are used linearly, and that linearity is maintained throughout the definition of the interpreter.

We present SeLoC: a relational separation logic for verifying non-interference of fine-grained concurrent programs in a compositional way. SeLoC is more expressive than previous approaches, both in terms of the features of the target programming language, and in terms of the logic. The target programming language supports dynamically allocated references (pointers), higher-order functions, and fine-grained fork-based concurrency with low-level atomic operators like compare-and-set. The logic provides an invariant mechanism to establish protocols on data that is not protected by locks. This allows us to verify programs that were beyond the reach of previous approaches. A key technical innovation in SeLoC is a relational version of weakest preconditions to track information flow using separation logic resources. On top of these weakest preconditions we build a type system-like abstraction, using invariants and logical relations. SeLoC has been mechanized on top of the Iris framework in the Coq proof assistant.

All computers run software, such as operating systems, web browsers, and video games, which are used by billions of people around the world. Therefore, it is important to develop high-quality software, which is only possible through interactive programming systems that involve programmers in the exchange of correct and responsive feedback. Fortunately, for many general-purpose programming languages, integrated development environments provide interactive programming systems through code editors and editor services.

Continuation marks enable dynamic binding and context inspection in a language with proper handling of tail calls and first-class continuations. The simplest and most direct use of continuation marks is to implement dynamically scoped variables, such as the current output stream or the current exception handler. By exposing continuation marks to users of a programming language, more kinds of language extensions can be implemented as libraries without further changes to the compiler. Our new implementation of continuation marks for Chez Scheme (in support of Racket) makes dynamic binding and lookup constant-time and fast and preserves the performance of Chez Scheme’s first-class continuations.

Compilation time is an important factor in the adaptability of a software project. Fast (incremental) recompilation enables cheap experimentation with changes to a project, as those changes can be tested quickly. Despite the benefits of an incremental compiler, such compilers are usually not the default. Published research on incremental compilation often shows how to build an incremental compiler from the ground up, based on a programming language that is well-suited for such a compilation scheme. We have found in our own work that when the first compiler for a language is not incremental, and language features are not developed with that incremental compiler in mind, it can be hard to develop such a compiler at a later time. We address this problem by developing a compiler design approach that reuses parts of an existing non-incremental compiler to lower the cost of building an incremental compiler. The key idea on which we build our incremental compiler is that we use an incremental build system internally to wire together the components we extract from the original compiler. We demonstrate our design approach on the Stratego programming language.

Applicative functors and monads have conquered the world of functional programming by providing general and powerful ways of describing effectful computations using pure functions. Applicative functors provide a way to compose independent effects that cannot depend on values produced by earlier computations, and all of which are declared statically. Monads extend the applicative interface by making it possible to compose dependent effects, where the value computed by one effect determines all subsequent effects, dynamically.

Nix is a purely functional build system: it builds immutable artifacts from a description in a simple purely functional DSL. It is used on its own and as the basis for NixOS, a Linux distribution with a declarative configuration model. In this talk I’ll reflect on the successes and failures of the Nix DSL: why it makes sense to use a DSL over a general-purpose language, but also why a sufficiently powerful DSL turns out to be both a blessing and a curse.

On the occasion of the PhD defense of Gabriel Konat, we are organizing a symposium on Build Systems with talks by Eelco Dolstra (Tweag I/O), Andrey Mokhov (Newcastle), Jeff Smits (TU Delft), Matthew Flatt (Utah) and Sebastian Erdweg (Mainz) followed by the defense itself.

Refactoring is the process of changing the internal structure of software to improve its quality without modifying its external behavior. Empirical studies have repeatedly shown that refactoring has a positive impact on the understandability and maintainability of software systems. However, before carrying out refactoring activities, developers need to identify refactoring opportunities. Currently, refactoring opportunity identification heavily relies on developers’ expertise and intuition.

In this paper, we investigate the effectiveness of machine learning algorithms in predicting software refactorings. More specifically, we train six different machine learning algorithms (i.e., Logistic Regression, Naive Bayes, Support Vector Machine, Decision Trees, Random Forest, and Neural Network) with a dataset comprising over two million refactorings from 11,149 real-world projects from the Apache, F-Droid, and GitHub ecosystems.

The resulting models predict 20 different refactorings at class, method, and variable levels with an accuracy often higher than 90%. Our results show that (i) Random Forests are the best models for predicting software refactoring, (ii) process and ownership metrics seem to play a crucial role in the creation of better models, and (iii) models generalize well in different contexts.

This seminar talk is a rehearsal of my talk “Taalgebaseerde softwareveiligheid” at the KNAW symposium VERIFICATIE VAN SOFTWARE: ERG COMPLEX MAAR IN IEDERS BELANG.

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.

With the increasing complexity of software and hardware components used in real-time cyber-physical systems (CPS), the gap between the state-of-the-art timing-analysis research and the state-of-practice in industry is rapidly growing. In this research, I have focused on closing this gap by designing an efficient and accurate formal timing-analysis framework to derive the worst-case response time bounds of real-time CPS. This is done by exploring the space of possible execution scenarios (and schedules) in the presence of uncertainties on the processes’ execution and arrival times. This talk introduces an analysis framework and explain how it can be used to solve complex timing-analysis problems. In this talk, I will also introduce one of our recent works on analyzing the timing behavior of programs written in Timed C programming language using our timing-analysis framework.

The generation of suitable test data is an essential part of property based testing. Obtaining test data is simple enough when there are no additional constraints, however things become more complicated once we require data with a richer structure, for example well-formed programs when testing a compiler. We observe that we can often describe constrained data as an indexed datatype. By generating values of the indexed datatype that describes a set of constrained test data, we simultaneously obtain a way to generate the constrained data itself. To achieve this goal, we consider three increasingly expressive type universes: regular types, indexed containers and indexed descriptions. We show how generators can be derived from codes in these universes, and for regular types and indexed descriptions we show that these derived generators obey a completeness property. We implement the generic generator for indexed descriptions in Haskell, and use this implementation to generate constrained test data, such as well-typed lambda terms.

Statix is a language which generates a type checker from a declarative specification. However, Statix is not fast enough for quick feedback in IDEs because it always has to reanalyze all files. In this thesis, we improve the analysis time of Statix by applying the ideas of separate compilation to create a model for incremental analysis. Statix uses a scope graph for representing the scoping and declarations of a project. We split the scope graph over multiple smaller modules which can be analyzed in isolation. Our model automatically detects dependencies between modules and supports creating scope graph diffs to determine modules affected by changes with high precision. The modules from our model can be solved in parallel, already yielding performance improvements of up to 40% compared to the original implementation. Finally, we implement an optimistic strategy with our model and show that it is effective whenever changes are small, reducing analysis time by up to 5 times for large projects.

An overview of research problems and methods in programming languages research.

Session types are a type-based approach for communication correctness in message-passing, concurrent programs: a session type specifies what should be exchanged along a communication channel and when. Session types have been originally developed as typing disciplines for processes in the pi-calculus, the paradigmatic calculus of interaction and concurrency.

Programming is hard. This is proven again and again by the numerous bugs, vulnerabilities, and other weird behaviours in the software we use every day. Dependently typed programming languages such as Agda allow the programmer to avoid many of these problems by encoding properties of programs in their types and statically checking that they hold. Compared to other tools for program verification, dependently typed languages are unique because they can be used both as a programming language and as an interactive proof assistant. In particular, the same techniques used for writing programs can also be used for writing proofs about these programs. Dependent pattern matching (Coquand, 1992) is one such technique for writing programs and proofs in dependently typed languages. It combines the intuitive notation of pattern matching from functional languages such as Haskell and ML with the mathematical techniques of case analysis and induction. Dependent pattern matching relies on a unification algorithm to specialize the type of each equation and automatically rule out impossible cases. Thanks to this unification algorithm, definitions by dependent pattern matching are often much shorter and easier to read compared to those written using other more primitive techniques. However, the original formulation of dependent pattern matching by Coquand is incompatible with new versions of dependent type theory such as homotopy type theory (HoTT). The source of this incompatibility lies in the unification algorithm employed for case splitting, which implicitly relies on two axioms – uniqueness of identity proofs and injectivity of type constructors – that are not permissible in HoTT. I present a new proof-relevant framework for reasoning formally about unification in a dependently typed setting. In this framework, each unification rule not only simplifies the equations but also produces evidence of its correctness. This evidence guarantees that all unification rules are correct by construction without relying on any axioms, and also gives a computational characterization to each unification rule. Based on these ideas, I implemented a complete overhaul of the algorithm for checking definitions by dependent pattern matching in Agda. My new implementation fixes a substantial number of issues in the previous version, and is at the same time more permissive than the old ad-hoc restrictions. Thus it puts the whole system back on a strong foundation. In addition, my work has already been used as the basis for other implementations of dependent pattern matching, such as the Equations package for Coq and the Lean theorem prover.

Side-effect are ubiquitous in programming. Examples include mutable state, exceptions, non-determinism, and user input. Algebraic effects and handlers are an approach to programming that gives a structured way of programming with effects. Each effect in a system with algebraic effects is defined by a set of operations. These operations can then be called anywhere in a program. Using a handler we can give an interpretation for the operations used. Unfortunately we are unable to express dynamic effects using regular algebraic effects, such as the dynamic creation of mutable references. Extending algebraic effects with effect instances enables us to express dynamic effects. These effect instances can be dynamically created and operations called on them are distinct from the same operation called on a different instance. Without a type system effect instances may result in runtime errors, because operation calls may be left unhandled. Because of their dynamic nature it is hard to give a type system for effect instances. In this thesis we present a new language, Miro, which extends algebraic effects and handlers with a restricted form of effect instances. We introduce the notion of an effect scope which encapsulates the creation and usage of dynamically created effect instances. We give a formal description of the syntax and semantics of Miro. We also give a type system which ensures that all operation calls are handled, so that there will be no runtime errors because of unhandled operation calls. Because effect instances can still escape their effect scope, in computationally irrelevant parts, we encounter difficulties in proving type safety for Miro. We discuss these difficulties and give a possible approach to prove type safety in the future.

Context: Updating an old result by selective re-execution of the inconsistent parts of some computation is usually faster than recomputing everything. Incremental build systems and interactive development pipelines use this technique to speed up feedback. They consist of different tasks. These tasks form a graph by depending on the environment and the result of other tasks. To re-execute a build requires an incremental build algorithm to find and re-execute inconsistent tasks. This can be done by traversing the dependency graph top down. When the mutations to the input environment are known in advance a build algorithm can avoid graph traversal. Thereby scaling with the size of a change instead of the size of the graph. Another important distinction between incremental build systems is their ability to handle dynamic dependencies. That is, dependencies that are discovered during a build. PIE is a bottom-up build algorithm that supports dynamic task dependencies. It schedules and executes inconsistent tasks without traversing the entire dependency graph. The current PIE algorithm is capable of adding dynamic task dependencies. However, it does not process removing dynamic task dependencies. This preserves consistency, but limits scalability over time. Each detached task is still scheduled and executed by the bottom up algorithm.

Programmable Logic Controllers (PLCs) are used to control large scale systems with thousands of I/O devices. Writing and maintaining the logic for each of these is a cumbersome task, which is well suited to be abstracted through templating. For this purpose, CERN developed the Unicos Application Builder (UAB). While UAB is successful at templating, it provides no guarantees over the validity of the outcome, leading to erroneous generated code. This is where SCL-T comes in. It builds on the foundation of UAB to facilitate meta-programming for Siemens’ SCL. Unlike its predecessor, it guarantees syntactic correctness and also draw conclusions regarding the semantic validity of the generated code. Its architecture has been designed in such a way that support for other PLC languages can be added using the same meta-language, reducing the cost of a having a meta-programming language tailored for a specific PLC language.

Build systems are awesome, terrifying – and unloved. They are used by every developer around the world, but are rarely the object of study. In this paper we offer a systematic, and executable, framework for developing and comparing build systems, viewing them as related points in landscape rather than as isolated phenomena. By teasing apart existing build systems, we can recombine their components, allowing us to prototype new build systems with desired properties.

Programming languages are one of the key components of computer science, allowing programmers to control, define, and change the behaviour of computer systems. However, they require considerable effort to design, implement, maintain, and develop them. Fortunately, declarative approaches can be used to define programming languages facilitating their development and implementation.

Static analyses deduct information about programs at compile time, for example, to provide feedback to developers, to find bugs, or to enable compiler optimizations. While static analysis is generally well-understood, the static analysis of program transformations has not seen much attention. The main challenge in developing a static analysis for program transformations is designing good abstractions that capture relevant information about the generated code. However, a complete static analysis must handle many other aspects of the transformation language, such as backtracking and generic traversals, as well as analysis-specific concerns, such as interprocedurality and fixpoints. This deflects attention. We propose a systematic approach to design and implement static analyses for program transformations that isolates the abstraction for generated code from other analysis aspects. Using our approach, analysis developers can focus on the design of abstractions for generated code, while the rest of the analysis definition can be reused. We show that our approach is feasible and useful by developing three novel inter-procedural analyses for the Stratego transformation language: a singleton analysis for constant propagation, a sort analysis for type checking, and a locally-illsorted sort analysis that can additionally validate type changing generic traversals.

Much of the Big Data hype focuses on the size of data and on the use of ML/AI to get something out of the data and on the programming technologies and infrastructure to deal with size, ML, and AI. Our research focuses on a complementary problem: the ontological semantics of data and how to use it for querying data programmatically and to help programmers in the tradition of static typing. In this talk, I present two strongly connected pieces of work: i) $\lambda_{\mathit{DL}}$ – a lambda calculus with description logic-aware type system and means of querying semantic data (‘triples’); ii) a completed language integration such that description logic and a subset of the standardized Sparql language are embedded into Scala. The integration reuses existing components – triple store, ontological reasoner, and Sparql query engine – and it extends the Scala type system appropriately.

Editor services assist programmers to more effectively write and comprehend code. Implementing editor services correctly is not trivial. This presentation focuses on our paper, which discusses 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.

In this talk I shall review the development of ideas of some of the classical approaches to generalised parsing, together with their associated problems, and I will discuss some of the most recent developments in our generalised LL parser family.

This work brings together aspects of structural operational semantics (SOS) and attribute grammars (AGs) for the concise specification of the typing and evaluation of programs that also handle error cases in an non-obtrusive way. SOS inference rules provide concise easy-to-read specifications, and they are a convenient formalism for reasoning about meta-theoretic properties. They are typically less useful for generating compilers and interpreters because they are, in a sense, incomplete. For typing, the inference rules provide a derivation only for type-correct programs; for evaluation, they provide a complete trace only for programs without run-time errors. There is no useful feedback to the programmer when their programs has typing or evaluation errors. AGs, however, are complete in that they compute attribute values for any syntactically correct tree, but the management of error conditions and error messages can clutter the specification, making it harder to read and reason about. Monads in functional programming provide a means for managing errors in computations, but the explicit use of monads, in the form of returns, binds, and do-notations, also clutter to specification. We describe a method for ``monadifying’’ an AG specification such that most equations defining attribute values are a direct transcription of SOS inference rules and the monadic constructs are only used when program errors are detected. We demonstrate this technique for concise typing and error reporting and easy specification of non-deterministic evaluation of expressions.

Attribute grammars were invented in 1968 by Donald Knuth as a formalism for specifying the semantics of context free languages. Attributes decorate syntax tree nodes to indicate, for example, the type of an expression or the environment for looking up identifier types or values. Equations over attributes determine these values. Since then the formalism’s popularity had waxed and waned but has been continually extended with new features to become an expressive paradigm for specifying many kinds of analyses and translations of programming languages. This talk will cover several of these extensions; including higher-order attributes, in which attributes can themselves be syntax trees, reference attributes, in which attributes are references to other nodes in the decorated tree, and forwarding, a mechanism that supports the composition of language extension specifications.

Developing distributed systems is a decades-old problem. Programming languages are a fundamental tool to face the complexity of such a scenario. Distributed applications are traditionally composed by separate modules, which are often written in different programming languages (e.g., JavaScript and Java). Such modules react to events, like user input or monitoring, and produce new events for the other modules. Separation into modules requires time-consuming cross-language integration and forces developers to manually implement low level communication details. Modularization across network boundaries may also result in obscure distributed data flows scattered among multiple modules, hindering reasoning about the system as a whole.

Software is used in every corner of our society, and deployed at ever-increasing scale and complexity. The challenges of producing reliable software are compounded by a wide variety of commonplace programming concerns, including mutable shared state, dynamic memory management, (fine-grained) concurrency, asynchronous and distributed communication and weak memory architectures. Formal verification research offers rich techniques for reasoning in these complex settings, but their application is often difficult in practice, both due to conceptual overhead and the substantial effort required in constructing a correct proof.

In this talk, I will present pretend synchrony, a new approach to verifying distributed systems, based on the observation that while distributed programs must execute asynchronously, we can often soundly treat them as if they were synchronous, when verifying their correctness. To do so, we compute a synchronization, a semantically equivalent program where all sends, receives, and message buffers, have been replaced by simple assignments, yielding a program that can be verified using Floyd-Hoare style verification conditions and SMT. We have implemented our approach as a framework for writing verified distributed programs in Go. Pretend synchrony allows us to develop performant systems while making verification of functional correctness simpler by reducing manually specified invariants by a factor of 6, and faster, by reducing checking time by three orders of magnitude.

Security analysis is a validating analysis that verifies that (highly) confidential information in a program does not flow to variables that may also store values of lower confidentiality. If such flows are possible, the program is rejected and a security type error message is provided.

An inductive definition is a way to define a predicate by an expression which may contain the predicate itself. The predicate is interpreted by the least fixed point of the defining equation. Inductive definitions are important in computer science, since they can define useful recursive data structures such as lists and trees. Inductive definitions are important also in mathematical logic, since they increase the proof theoretic strength. Martin-Lof’s system of inductive definitions given in 1971 is one of the most popular system of inductive definitions.

In the paper ‘Scopes Describe Frames’ by Bach Poulsen et al. the scopes-as-frames paradigm was introduced. In this paradigm there is a correspondence between the scope graph of a program and its run-time memory layout. As an effect, static resolution paths in the scope graph correspond to dynamic memory access paths. Precisely this paradigm lies at the core of the Frame VM: A virtual machine that is being developed to both explore the correspondence between scopes and frames, and as a way to ease code generation for language designers.

Session types statically guarantee that communication complies with a protocol. However, most accounts of session typing do not account for failure, which means they are of limited use in real applications—especially distributed applications—where failure is pervasive.

For software developers, any non-trivial program quickly grows to a scope where it is difficult to ascertain whether the program actually does what the programmer intended. There have been several solutions for this problem, such as writing tests that automatically assert facts about the execution of the program. Another approach is the writing of abstract interpreters that analyze the system under test for properties such as type safety. Proving these abstract interpreters to be sound and correct is cumbersome and often omitted.

Graph-structures such as shared packed parse forests (SPPFs) and annotated terms (ATerms) typically form the output of a generalised parser. This talk introduces sets of binary subtree representations (BSR sets) as an alternative and shows how BSR sets can be generated by a generalised parser. The set-based output removes the clerical overhead associated with graph construction, simplifying the definition of the parser. This talk further demonstrates how the potentially many derivations embedded in a BSR set can be extracted, interpreted, or discarded in a post-processing phase.

Formal Verification is quite an undertaking, even for simple systems, with specifications and approaches quickly growing beyond the scope of which one can maintain a proper overview. This is doubly true for more complicated systems, like those utilizing concurrency and distributed communication; as such it is imperative to employ intuitive methods to alleviate possible overhead.

Research into C verification often ignores that the C standard leaves the evaluation order of expressions unspecified, and assigns undefined behavior to write-write or read-write conflicts in subexpressions—so called “sequence point violations”. Undefined behavior may cause a program to crash or to have arbitrary results, so it is essential to make sure that C programs are free of undefined behavior for any expression evaluation order.

One promising way to improve the security of legacy software is to provide hardware support for programmable runtime reference monitoring at the level of individual hardware instructions, based on metadata tags attached to register and memory contents. This technique has been demonstrated to enforce policies such as memory safety and taint tracking with reasonable efficiency, while making minimal assumptions about the correctness of the system software.

This paper presents a framework for the static specification and safe programming of message passing protocols where the number and kinds of participants are dynamically instantiated.

Information systems are systems for the collection, organization, storage, and communication of information. Information systems aim to support operations, management and decision-making. In order to do this, these systems filter and process data according to business logic to create new data. Typically these information systems contain large amounts of data and receive frequent updates to this data. Over time requirements for information systems change, from the decision making logic to the number of users interacting with the system. As organizations evolve, so must their information systems. Our reliance on information systems to make decisions and the ever changing requirements poses the following challenges for information system engineering. Validatability: how easy is it for information system developers to establish that a system ‘does the right thing’? Traceability: can the origin of decisions made by the system be verified? Reliability: can we trust the system to consistently make decisions and not lose our data? Performance: can the system keep responding promptly to the load of its users? Availability: can we trust that the system performs its functionality all of the time?And finally, modifiability: how easy is it to change the system specification when requirements change?In this dissertation we show the feasibility and usefulness of declarative programming for information systems in light of these challenges. Our research method is design research. This iterative method repeats four phases: analysis, design, evaluation, and diffusion. We analyze the challenges of information system engineering, design a new programming language to address these, evaluate our new programming language in practice, and diffuse our knowledge through scholarly articles. This resulted in four new declarative languages: the Relations language, IceDust, IceDust2, and PixieDust. Our contributions can be summarized by the new features of these languages. Native multiplicities, bidirectional relations, and concise navigation improve information system validatability and modifiability over object-oriented and relational approaches. Derived attribute values improve traceability. Incremental and eventual computing based on path analysis and calculation strategy switching improve information system modifiability without sacrificing performance and availability over object-oriented and relational approaches. Calculation strategy composition improves validatability, modifiability, and reliability over reactive programming approaches. And finally, Bidirectional derived relations improve information system validatability over relational approaches. The results of this dissertation can be applied in practice. We applied IceDust2 to the learning management information system WebLab. We found that validatability, traceability, reliability, and modifiability were considerably improved while retaining similar performance and availability. Moreover, the fact that IceDust and PixieDust work in different domains, business logic and user interfaces respectively, suggests that our language features could be applied to more domains.

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 semantics editor services, those that use the semantic model of a program. The specification of refactorings is a common subject of study, but many other semantics editor services have received little attention.

Part of the Symposium on Declarative Programming

Conventional collaboration among programmers relies on optimistic locking of files (through version control), perhaps enhanced with “soft” pessimistic locking via informal communication channels (e.g., by chatting things like “I will be working on file X for the rest of the day, so don’t you touch it”). Optimistic locking enables parallel work, at the price of manually merging competing edits (edit conflicts) at update or commit time. Merging edits is an unpopular and, in any case, error-prone task; yet, “hard” pessimistic locking of files does not appear to be a viable alternative.

Distributed applications are traditionally developed as separate modules, often in different languages, which react to events, like user input, and in turn produce new events for the other modules. Separation into components requires time-consuming integration. Manual implementation of communication forces programmers to deal with low-level details. The combination of the two results in obscure distributed data flows scattered among multiple modules, hindering reasoning about the system as a whole.

On the occasion of the PhD defense of Daco Harkes, we are organizing a symposium on Declarative Programming with talks by Görel Hedin (Lund), Friedrich Steimann (Hagen), Guido Salvaneschi (Darmstadt), Hendrik van Antwerpen (Delft), followed by the defense itself.

It can be a huge effort to give a complete formal specification of a major programming language, and then to update it when the language evolves. This appears to discourage most language developers from exploiting formal specifications to document their language designs. One of the main aims of the CBS meta-language, designed by the PLanCompS project, is to significantly reduce the required effort. A unique feature of CBS is that it comes together with a substantial library of reusable components called funcons (fundamental programming constructs). The semantics of each funcon is pre-defined, so specifying a translation of a language to funcons defines the language semantics; this can be significantly less effort than direct specification. When a language evolves, the translation of unaffected language constructs does not change. Crucially, adding new funcons to the library does not require changes to the definition or use of the previous funcons. In this talk, we demonstrate how reuse and co-evolution in CBS work: we first specify a small pure functional programming language by translation to funcons, then extend the language with mutable variables and concurrent threads. CBS is supported by an IDE (implemented in Spoofax) and by a Haskell package for generating modular funcon interpreters from funcon definitions.

In this talk I present our recent work on proving the safety and completeness of a semantics for disambiguation of context-free expression grammars with associativity and priority declarations.

Logical relations have been used to certify the soundness of languages and type systems. Iris offers an suitable framework for this approach, where it was used to give guarantees about Rust. During my internship, I focused on another major property, termination, and wanted see if Iris could be used to reason about termination. In this talk I will present my main result: a termination proof, in Iris, for a language with recursive types and references. I will also discuss possible future work, mainly in the direction of modularity.

Constraint Programming (CP) is a capable and flexible approach to combinatorial optimisation. This talk will outline the open source CP modelling language MiniZinc (www.minizinc.org). MiniZinc is a high-level, declarative, solver-agnostic language that supports the CP paradigm of separating model specification from model solving. MiniZinc compiles to a lower-level language called FlatZinc, through which it interfaces to several commercial and open-source backend solvers

The metatheory of the Scala core type system (DOT), first established recently, is still hard to extend, like other systems combining subtyping and forms of dependent types. Soundness of important Scala features remains an open problem in theory and in practice. To obtain a more extensible metatheory, in ongoing work we prove in Coq soundness of DOT semantically. This is challenging, because in DOT variables can be in scope in their own type, objects can define mutually recursive and impredicative type members, and can contain evidence of subtyping relations that must be sound. We address these challenges by novel applications of step-indexing, as supported by the Iris logic. Our proof clarifies difficulties in past proofs; ongoing work on extensions, such as paths, appears encouraging.

Session types are a formal method to describe communication protocols between two or more actors. Protocols that type check are guaranteed to respect communication safety, linearity, progress, and session fidelity. Basic session types, however, do not in general guarantee anything about the contents of messages, while real-life applications of structured communication, such as money transfers at the ING bank, could benefit greatly from content safety. In this work, we show how to state, verify, and run session-typed protocols with dependent variables in Idris, using Idris’ ST library.We also present an extension to the protocol description language Scribble. Scribble is a language for defining high-level global protocols between multiple actors and comes with a tool that automatically generates type signatures of local protocols for each actor in Java, in a way that these type signatures ensure that local actors follow the global protocol specification. We describe a new variant of the Scribble language which adds support for dependent variables, and a new tool for automatically generating Idris type signatures of local protocols for actors in a way that enforces dependent invariants.

Connected and Autonomous Vehicles (CAV) are taking a central position in the landscape of intelligent mobility, and their rigorous verification and validation is one of the main challenges in their public deployment and social acceptance. Conformance testing is a rigorous verification technique that has been widely tried in various critical applications. In this talk, we examine the adaptations and extensions of the notions of conformance and model-based testing techniques that make them suitable for application in the CAV domain. We present how the extended techniques can be used in the design of connected vehicle functions and verify various design decisions.

Large companies suffer from the increasing complexity that exists in their software systems. Evolving their software
becomes even harder if we consider that a change in one system can affect several other parts of their software architecture. In particular, banks, that always need to comply with regulations, have to constantly make changes in their software to reflect these changes. ING is a primary example that currently tries to find a solution to these problems through the use of model driven development and more specifically code generation. In particular, they have created a Domain Specific Language called Maverick to specify the requirements / business logic and through the usage of code generators to automatically generate their entire codebase from these Maverick specifications. Code generators as any other software artifact is not bug free, meaning that testing code generators is of paramount importance. However, testing code generators is not straightforward as their output is another program that besides syntactic structure also has behavior. Many formal approaches have been developed that try to formally prove the correctness of code generators. Nevertheless, the complexity and scalability issues that these approaches face make them infeasible in practice. This thesis presents a testing approach that leverages a definitional interpreter to test code generators. We evaluate and show the practicability of our approach using Maverick specifications developed by ING and we conclude that our proposed method can address many of the issues that formal approaches face.

To make the first-year course Reasoning & Logic more tangible, we added a project to it. In the project, students write formal specifications that are automatically checked by Z3. I will explain the setup and results of this project and what conclusions we have drawn from using Z3 with 900 first-year students.

Slowly but steadily Technolution B.V. is adopting Rust as a new programming language for mission-critical and secure software. This talk will explain what Rust is all about and why a company that has been developing software and electronics for over 30 years in languages like C and Java is adding another language to its portfolio.

When using an integrated development environment, it is desirable to get real-time feedback on the correctness of the program. That is, we want to see the results of the type checker in real-time. However, type checking can take a long time, especially when the subject program is large. To be able to provide real-time results, we need to incrementalize the type checker. This way, when a program changes, we only need to recalculate results for the changed portion of the program, and everything that depends on it. In this thesis, we discuss how we used IncA to implement a type checker for Rust. IncA is a domain specific language for the definition of incremental program analyses: analyses written in IncA are automatically incrementalized. We show in our evaluation that our type checker updates results significantly faster than its non-incremental counterpart. While we were able to successfully implement many of Rust’s features, there are some parts we were unable to implement, and we show why that is the case.

Many program transformation languages simplify the implementation of program transformations. However, they give only weak static guarantees about the generated code such as well-sortedness. Well-sortedness guarantees that a program transformation does not generate syntactically ill-formed code, but it is too imprecise for many other scenarios. In this paper, we present a static analysis that allows developers of program transformations to reason about their transformations on a more fine-grained level, namely that of syntactic shape. Specifically, we present an abstract interpreter for the Stratego program transformation language that approximates the syntactic shape of transformed code using regular tree grammars. As a baseline, we also present an abstract interpreter that guarantees well-sortedness. We prove parts of both abstract interpreters sound.

Tamás Szabó will practise this talk: https://2018.splashcon.org/event/splash-2018-oopsla-incrementalizing-lattice-based-program-analyses

Hendrik van Antwerpen will practise this talk: https://2018.splashcon.org/event/splash-2018-oopsla-scopes-as-types

We present a tool architecture that supports migrating custom domain-specific language (DSL) implementations to a language workbench. We demonstrate an implementation of this architecture for models in the domains of defining component interfaces (IDL) and modeling system behavior (OIL) which are developed and used at a digital printer manufacturing company. Increasing complexity and the lack of DSL syntax and IDE support for existing implementations in Python based on XML syntax hindered their evolution and adoption. A reimplementation in Spoofax using modular language definition enables composition between IDL and OIL and introduces more concise DSL syntax and IDE support. The presented tool supports migrating to new implementations while being backward compatible with existing syntax and related tooling.

CBS is a component-based semantic framework that aims to facilitate and encourage formal specification of programming languages. The main idea is to specify the intended behaviour of language constructs by translating them to so-called ‘funcons’: fundamental constructs for expressing control flow, data flow, binding, storing, interaction, function abstraction, etc. The definition of a funcon is a highly reusable component of language specifications. The beta-release of an initial library of funcons is available online [https://plancomps.github.io/CBS-beta]. This talk starts by introducing CBS and the funcons library. It then explains the current tool support for CBS, which has been partly implemented in Spoofax.

20 years ago I presented the paper “Building program optimizers with rewriting strategies” at ICFP 1998. The paper described the design of a language for program transformation based term rewriting with rewriting strategies that can be defined using a set of combinators. The language was later named Stratego.

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.

Abstract interpretation is a technique for developing static analyses. Yet, proving abstract interpreters sound is challenging for interesting analyses, because of the high proof complexity and proof effort. To reduce complexity and effort, we propose a framework for abstract interpreters that makes their soundness proof compositional. Key to our approach is to capture the similarities between concrete and abstract interpreters in a single shared interpreter, parameterized over an arrow-based interface. In our framework, a soundness proof is reduced to proving reusable soundness lemmas over the concrete and abstract instances of this interface; the soundness of the overall interpreters follows from a generic theorem.

A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making separation-logic proofs look and feel like ordinary Coq proofs. However, IPM is tied to a particular separation logic (namely, Iris), thus limiting its applicability.

Incremental build systems are essential for fast, reproducible software builds. Incremental build systems enable short feedback cycles when they capture dependencies precisely and selectively execute build tasks efficiently. A much overlooked feature of build systems is the expressiveness of the scripting language, which directly influences the maintainability of build scripts. In this paper, we present a new incremental build algorithm that allows build engineers to use a full-fledged programming language with explicit task invocation, value and file inspection facilities, and conditional and iterative language constructs. In contrast to prior work on incrementality for such programmable builds, our algorithm scales with the number of tasks affected by a change and is independent of the size of the software project being built. Specifically, our algorithm accepts a set of changed files, transitively detects and re-executes affected build tasks, but also accounts for new task dependencies discovered during building. We have evaluated the performance of our algorithm in a real-world case study and confirm its scalability.

Incremental verification means that after making small changes to a program, annotations, and specifications, only a small part of the verification needs to be re-evaluated. As an extension of this: making a small change to a verification technique should also require only part of any verification to be re-evaluated. For this to work, we need a suitable domain specific language for verification techniques. A requirement for this language is that conceptually small changes should be likely to result in small code changes.

Language Workbenches are instruments developers use to create new domain-specific languages. They provide tools to rapidly develop, test and deploy new languages. Currently, workbenches support deployment in desktop-based integrated development environments. Setting up these environments can be a hurdle for the often non-technical users of these languages. Web-Based IDEs could be a solution in this case, but workbenches are currently not able to deploy languages in these environments.

Static analyses are best known for detecting errors at compile time and thus helping developers to write correct code. That’s an honorable quest and not for nothing static analysis is sometimes referred to as lightweight verification. But static analysis has a second quest of equal importance: to aid program understanding. Development tools such as IDEs use information computed by static analyses to explain the program to the developer (variable v has type int, variables v1 and v2 point to the same object), to provide exploration functionality (jump to declaration, find call sites), to guide developers (uninitialized read, dead code), and to provide sophisticated edit actions (refactorings). IDEs must provide all these features without interrupting the workflow of the developer. In particular, IDEs must react quickly to code changes. That is, the underlying static analyses need to be incremental.

We present ReLoC: a logic for proving refinements of programs in a language with higher-order state, fine-grained concurrency, poly- morphism and recursive types. The core of our logic is a judgement e ≾ e’ : τ, which expresses that a program e refines a program e’ at type τ. In contrast to earlier work on refinements for languages with higher-order state and concurrency, ReLoC provides type- and structure-directed rules for manipulating this judgement, whereas previously, such proofs were carried out by unfolding the judgement into its definition in the model. These more abstract proof rules make it simpler to carry out refinement proofs. Moreover, we introduce logically atomic relational specifications: a novel approach for relational specifications for compound expressions that take effect at a single instant in time. We demonstrate how to formalise and prove such relational specifications in ReLoC, allowing for more modular proofs. ReLoC is built on top of the expressive concurrent separation logic Iris, allowing us to leverage features of Iris such as invariants and ghost state. We provide a mechanisation of our logic in Coq, which does not just contain a proof of soundness, but also tactics for interactively carrying out refinements proofs. We have used these tactics to mechanise several examples, which demonstrates the practicality and modularity of our logic.

Coq supports a range of built-in tactics, which are engineered primarily to support backward reasoning. Starting from a desired goal, the Coq programmer can use these tactics to manipulate the proof state interactively, applying axioms or lemmas to break the goal into subgoals until all subgoals have been solved. Additionally, it provides support for tactic programming via OCaml and Ltac, so that users can roll their own custom proof automation routines.

In this talk I will present Statix, a meta-language for writing type checkers. Statix is a constraint language with built-in support for scope graphs. It builds on the concepts of the constraint language underlying NaBL2, but increases expressivity by generalizing the constraints and aspects of scope graph resolution. I will show examples to highlight interesting language features, and discuss our follow-up efforts.

Information system engineering is challenging as it is non-trivial to build information systems that are validatable, traceable, reliable, available, modifiable and performant at the same time. The aim of the IceDust research is to address these challenges in information system engineering. The combination of these challenges limits the scope to reactive or incremental computing, and domain-specific languages.

An immutable multi-map is a many-to-many map data structure with expected fast insert and lookup operations. This data structure is used for applications processing graphs or many-to-many relations as applied in compilers, runtimes of programming languages, or in static analysis of object-oriented systems. Collection data structures are assumed to carefully balance execution time of operations with memory consumption characteristics and need to scale gracefully from a few elements to multiple gigabytes at least. When processing larger in-memory data sets the overhead of the data structure encoding itself becomes a memory usage bottleneck, dominating the overall performance.

PART I Testing Code Generators against Definitional Interpreters

Implementing the syntax and semantics of a new (domain-specific) programming language is a lot of work, which is worsened by the additional work needed to add support for the language to an editor such as Eclipse or VS Code. Lack of such support can impede language usability and adoption, as developers prefer different editors. However, supporting M editors for N languages requires M * N implementations to be built and maintained, which is known as the IDE portability problem. Portable editor services aim to reduce this to M + N implementations, which leads to the main question of this thesis: how can we make the editor services of languages portable across editors?

There are two kinds of static analyses for imperative programming languages such as the While-language - Value analyses that analyze values of the language, e.g., what range of numbers a numeric variable can hold, and effect analyses that analyze the effect of destructive updates, e.g., which variable definitions are reachable and have not been overridden.

LeQuest develops interactive e-training modules to improve the competence regarding medical technology of medical professionals. The medical technology is analysed by LeQuest to develop training modules, but the analysis process and writing associated information can be performed more efficiently. This would reduce the required time and resources which could be invested in additional trainings and quality improvements. In the end, this will lead to an improvement regarding the patient’s safety in health institutions. This work empirically evaluated the Spoofax Workbench by conducting an industrial case-study which consists of the design, implementation and evaluation of a domain-specific language (DSL). The LeQuest DSL is used as a tool for transforming the current analysis process into a more formalized process which does allow for objective observations, measurements and quantifiable information. Although the LeQuest DSL is not integrated in the current work-flow yet, the evaluation has shown that it is expected that the overall quality and efficiency of the analysis process will increase after the introduction of the DSL.

Testing is the most commonly used technique for raising confidence in the correctness of a piece of software, but constructing an effective test suite is expensive and prone to error. Property-based testing partly automates this process by testing whether a property holds for all randomly generated inputs, but its effectiveness depends upon the ability to automatically generate random test inputs. When using property-based testing to test a compiler backend, the problem becomes that of generating random pro- grams that pass the parsing and analysis phase. We present SPG (SPoofax Generator), a language-parametric generator of random well-formed terms. We describe three experiments in which we evaluate the effectiveness of SPG at discovering different kinds of compiler bugs. Furthermore, we analyze why the generator fails to detect certain compiler bugs and provide several ideas for future work. The results show that random testing can be a cost-effective technique to find bugs in small programming languages (such as DSLs), but its application to practical programming languages requires further research.

A popular form of software reuse is the use of open source software libraries hosted on centralized code repositories, such as Maven or npm. Developers only need to declare dependencies to external libraries, and automated tools make them available to the workspace of the project. Recent incidents, such as the Equifax data breach and the leftpad package removal, demonstrate the difficulty in assessing the severity, impact and spread of bugs in dependency networks. While dependency checkers are being adapted as a counter measure, they only provide indicative information.

Context-free grammars are widely used for language prototyping and implementation. They allow formalizing the syntax of domain-specific or general-purpose programming languages concisely and declaratively. However, the natural and concise way of writing a context-free grammar is often ambiguous. Therefore, grammar formalisms support extensions in the form of declarative disambiguation rules to specify operator precedence and associativity, solving ambiguities that are caused by the subset of the grammar that corresponds to expressions.

“Science and the humanities are founded on integrity. It is one of the key principles of good scientific practice and therefore of every piece of research. Only science performed with integrity can ultimately be productive science and lead to new knowledge. On the other hand, a lack of integrity can represent a threat to science, destroying the confidence of researchers in each other and that of the public in science; research is unthinkable without this confidence.” [cited from Safeguarding Good Scientific Practice]

DSL’s developed using language workbenches are often used by domain experts. Setting up a local development environment for a DSL can be challenging for these people. Web-based development environments could be a solution in this situation, but deploying runtimes for languages defined in a language workbench to these type of IDEs is still ongoing research.

The Unix diff utility that compares lines of text is used pervasively by version control systems. Yet certain changes to a program may be difficult to describe accurately in terms of modifications to individual lines of code. As a result, observing changes at such a fixed granularity may lead to unnecessary conflicts between different edits. This talk discusses a generic representation for describing transformations between algebraic data types. These representations can be used to give a more accurate account of modifications made to algebraic data structures – and the abstract syntax trees of computer programs in particular – as opposed to only considering modifications between their textual representations.

The static semantics of a programming language describes aspects such as program types, name resolution, or overload resolution. Static semantics can be described in terms of relations. For example, expressions are related to their types by a typing relation, and types are related to each other with a subtype relation. The meta-language NaBL2 allows the specification of static semantics by defining a relation over programs in terms of equality and name resolution constraints. However, expressing non-program-oriented relations such as type-based overloading, custom type relations such as structural subtyping, or name disambiguation was mostly impossible. In this talk we present Statix, a language to specify static semantics, that addresses these limitations. Statix is inspired by ideas from logic programming, and supports user-defined relations on top of builtin theories such as term equality and scope graph based name resolution. These relations are defined in terms of guarded simplification rules. We introduce the language using examples, showing cases such as type-based overloading, and structural record types with subtyping. We discuss some challenges related to the implementation of a sound solver for this language, and discuss directions for further work.

Session types are a formal method to describe communication protocols between two or more actors. Protocols that type check are guaranteed to respect communication safety, linearity, progress, and session fidelity. Basic session types, however, do not in general guarantee anything about the contents of messages, while real-life applications of structured communication, such as money transfers at the ING bank, could benefit greatly from content safety. In this work, we show how to state, verify, and run session-typed protocols with dependent variables in Idris, using Idris’ ST library.

Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. These projects include but are not limited to: verification of fine-grained concurrent data structures, logical-relations for relational reasoning, program logics for relaxed memory models, program logics for object capabilities, and a safety proof for a realistic subset of the Rust programming language. In this talk I will give an introduction to Iris and its implementation in Coq.

Algebraic effects and handlers provide a compositional way of structuring effectful programs. Dynamic instances increase the expressiveness of algebraic effects by allowing the creation multiple instances of an effect. We would like to design a type system for dynamic instances and prove its soundness.

Tamás and Sebastian have been working on IncA, a framework/DSL for implementing efficient incremental program analyses. Existing case studies for IncA only use relatively simple program analyses. To determine the suitability of IncA for more complex analyses, and for type checkers for real-world languages in particular, a type checker for the Rust language is implemented in IncA.

The result of an abstract interpreter is only useful if it is sufficiently precise. The output of Sven and Sebastian’s arrow-based abstract interpreter is necessarily limited given soundness and termination requirements. In this presentation I will outline my thesis: attempting to increase precision with a more precise representation of term shapes.

Rust is a new programming language, targeting system programming. One interesting feature is how it enforces memory safety and data race freedom, in the face of aliasing and mutability, using lifetimes and borrowing. In this talk we will see the main idea of the borrow checker and how we want to implement it in Spoofax.

SGLR parsing is an approach that enables parsing of context-free languages by means of declarative, concise and maintainable syntax definition. Existing implementations suffer from performance issues and their architectures are often highly coupled without clear separation between their components. This work introduces a modular SGLR architecture with several variants implemented for its components to systematically benchmark and improve performance. This work evaluates these variants both independently and combined using artificial and real world programming languages grammars. The architecture is implemented in Java as JSGLR2, the successor of the original parser in Spoofax, interpreting parse tables generated by SDF3. The improvements combined result into a parsing and imploding time speedup from 3x on Java to 10x on GreenMarl with respect to the previous JSGLR implementation.

Program analyses detect errors in code but have to trade off precision, recall, and performance. However, when code changes frequently as in an IDE, repeated re-analysis from-scratch is unnecessary and leads to poor performance. Incremental program analysis promises to deliver fast feedback after a code change by deriving a new analysis result from the previous one, and prior work has shown that order-of-magnitude performance improvements are possible. However, existing frameworks for incremental program analysis only support Datalog-style relational analysis, but not lattice-based analyses that derive and aggregate lattice values. To solve this problem, we present the IncAL incremental program analysis framework that supports relational analyses and lattice-based computations. IncAL is based on a novel algorithm that enables the incremental maintenance of recursive lattice-value aggregation, which occurs when analyzing looping code by fixpoint iteration. We realized strong-update points-to analysis and string analyses for Java in IncAL and present performance measurements that demonstrate incremental analysis updates within milliseconds.

Reference

Reference

Reference