Programming Languages Seminar

The PL group organizes a weekly lunch seminar on Wednesdays from 12:00 to 13:00 in which one of the group members or a visitor gives a talk. Occasionally we have `progress' lunches in which everyone gives an update about what they are doing. (See the seminar instructions to add an entry.)

Upcoming Talks

Past Talks

Symmetric Dependent Data and Codata Types
David Binder

Date: Wed, March 13, 2024
Time: 12:00
Room: Turing

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.

[more]
Universes and relative indexed monads for type safe syntax and semantics
Jaro Reinders

Date: Wed, December 20, 2023
Time: 12:00
Room: Turing

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.

[more]
​Julia, types, and property based testing
Valentin Bogad

Date: Wed, November 29, 2023
Time: 12:00
Room: Turing

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.

[more]
Proving and Disproving Equivalence of Functional Programming Assignments
Dragana Milovancevic

Date: Wed, October 25, 2023
Time: 12:30
Room: Turing

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.

[more]
Online Name-Based Navigation for Software Meta-languages
Peter Mosses (Delft University of Technology and Swansea University)

Date: Wed, October 18, 2023
Time: 12:00
Room: Turing 0.E420
Note: This is a rehearsal for a talk/demo at SLE 2023

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.

[more]
A Monadic Framework for Name Resolution in Multi-phased Type Checkers
Casper Bach Poulsen (Delft University of Technology)

Date: Wed, October 11, 2023
Time: 12:00
Room: Turing 0.E420
Note: This is a rehearsal for a talk/demo at GPCE 2023

Published paper
mophasco.pdf
[more]
Language-Parametric Reference Synthesis
Daniel Pelsmaeker (Delft University of Technology)

Date: Wed, September 20, 2023
Time: 12:00
Room: Turing 0.E420

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.

[more]
Dependent Type Checking Modulo Associativity and Commutativity
Lucas Holten (Delft University of Technology)

Date: Tue, September 12, 2023
Time: 10:00
Room: F 206, building 22 (Applied Physics), meeting room E3-1
Note: This is a Masters defense.

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.

[more]
...
Strategic Language Workbench Improvements
Jeff Smits (TU Delft)

Date: Fri, September 08, 2023
Time: 10:00
Room: Senaatszaal, Auditorium
Note: This is a PhD defense. The candidate's talk starts at 09.30.

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.

[more]
The Paradigm Shift in SE & PL Research & Teaching due to LLMs
Ralf Lämmel

Date: Thu, September 07, 2023
Time: 16:45
Room: Hall-C (29.02.050), Building 29, Echo

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.

[more]
Towards a Modular Metatheory for Extensible Languages
Eric Van Wyk

Date: Thu, September 07, 2023
Time: 16:00
Room: Hall-C (29.02.050), Building 29, Echo

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.

[more]
Invited Talks by Doctoral Committee Members
Ralf Lämmel, Eric Van Wyk

Date: Thu, September 07, 2023
Time: 16:00
Room: Hall-C (29.02.050), Building 29, Echo

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).

[more]
Formal semantics of declarative disambiguation rules
Luka Miljak

Date: Wed, September 06, 2023
Time: 12:00
Room: Turing 0.E420
Note: This is a talk on ongoing research

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?

[more]
Improving Agda’s module system
Ivar de Bruin (Delft University of Technology)

Date: Wed, July 05, 2023
Time: 14:00
Room: Room C, Building 29, Echo
Note: This is a Masters defense.

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.

[more]
Speeding up program synthesis using specification discovery
Jaap de Jong (Delft University of Technology)

Date: Tue, July 04, 2023
Time: 10:30
Room: Room C, Building 29, Echo
Note: This is a Masters defense.

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.

[more]
Bringing Formal Verification into Widespread Programming Language Ecosystems
Sára Juhošová (Delft University of Technology)

Date: Thu, June 29, 2023
Time: 09:00
Room: Echo Arena
Note: This is a Masters defense.

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.

[more]
Verified Reversible Programming for Verified Lossless Compression
James Townsend (University of Amsterdam)

Date: Wed, June 28, 2023
Time: 12:00
Room: Turing 0.E420

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.

[more]
Formalizing Access Modifiers using Scope Graphs: Ongoing Research Talk
Aron Zwaan (Delft University of Technology)

Date: Wed, May 10, 2023
Time: 12:00
Room: Turing 0.E420

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
[more]
Dependently Typed Languages in Statix
Jonathan Brouwer (Delft University of Technology)

Date: Wed, April 26, 2023
Time: 12:00
Room: Snijderszaal LB 01.010 (building 36)
Note: This is a Masters defense.

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.

[more]
Efficiently Executing User-Provided Graph Algorithms in a Graph Database
Daan de Graaf

Date: Wed, April 19, 2023
Time: 12:00
Room: Turing 0.E420

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.

[more]
Bootstrapping the Statix Meta-Language
Boris Janssen (Delft University of Technology)

Date: Mon, April 17, 2023
Time: 10:30
Room: Echo Arena
Note: This is a Masters defense.

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.

[more]
Spoofax at Oracle: Domain-Specific Language Engineering for Large-Scale Graph Analytics
Houda Boukham and Guido Wachsmuth

Date: Thu, April 06, 2023
Time: 12:45
Room: Echo Arena

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.

[more]
Stack graphs: Name resolution at scale
Douglas A. Creager, Hendrik van Antwerpen (Github)

Date: Wed, March 22, 2023
Time: 12:00
Room: Turing 0.E420

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.

[more]
Dependently Typed Languages in Statix
Jonathan Brouwer, Jesper Cockx, Aron Zwaan (TU Delft / PL)

Date: Wed, March 22, 2023
Time: 12:00
Room: Turing 0.E420

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.

[more]
Eating Your Own Dog Food: WebDSL Case Studies to Improve Academic Workflows
Danny Groenewegen, Elmer van Chastelet, Max de Krieger, Daniel A. A. Pelsmaeker (TU Delft / PL)

Date: Wed, March 15, 2023
Time: 12:00
Room: Turing 0.E420

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.

[more]
Conf Researchr: A Domain-Specific Content Management System for Managing Large Conference Websites
Danny Groenewegen, Elmer van Chastelet, Max de Krieger, Daniel A. A. Pelsmaeker, Craig Anslow (TU Delft / PL, Victoria University)

Date: Wed, March 15, 2023
Time: 12:30
Room: Turing 0.E420

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.

[more]
Scope Graphs: The Story so Far
Aron Zwaan, Hendrik van Antwerpen (TU Delft / PL)

Date: Wed, March 08, 2023
Time: 12:30
Room: Turing 0.E420

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.

[more]
Renamingless Capture-Avoiding Substitution for Definitional Interpreters
Casper Bach Poulsen (TU Delft / PL)

Date: Wed, March 08, 2023
Time: 12:00
Room: Turing 0.E420

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.

[more]
Using Spoofax to Support Online Code Navigation
Peter D. Mosses (TU Delft / PL)

Date: Wed, March 01, 2023
Time: 12:00
Room: Turing 0.E420

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.

[more]
Towards Modular Compilation using Higher-order Effects
Jaro Reinders (TU Delft / PL)

Date: Wed, March 01, 2023
Time: 12:30
Room: Turing 0.E420

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.

[more]
Aesop: White-Box Best-First Proof Search for Lean
Jannis Limperg (Vrije Universiteit Amsterdam)

Date: Wed, February 15, 2023
Time: 12:00
Room: Turing 0.E420

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.

[more]
Crafting Incremental Parallel and Self-Tracking Embedded Build Systems
Lucas (TU Delft)

Date: Wed, February 01, 2023
Time: 12:00
Room: Turing 0.E420

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).

[more]
Modular Dynamic Semantics Specification and Compilation
Jaro Reinders (TU Delft / PL)

Date: Thu, January 26, 2023
Time: 13:00
Room: Echo Arena
Note: This is a PhD Go/No-Go meeting

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.

[more]
To parse or to marshall, that is the question
Jurgen Vinju (CWI Amsterdam, TU Eindhoven)

Date: Wed, January 25, 2023
Time: 12:00
Room: Turing 0.E420

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?

[more]
Teaching Introduction to Proofs with Lean
Sina Hazratpour

Date: Wed, January 11, 2023
Time: 11:45
Room: Turing 0.E420

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.

[more]
Syntactical extensibility of proof assistants
Bohdan Liesnikov (TU Delft / PL)

Date: Wed, January 11, 2023
Time: 14:00
Room: Turing 0.E420
Note: This is a PhD Go/No-Go meeting

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

[more]
Computing Cohomology Rings in Cubical Agda
Thomas Lamiaux

Date: Wed, January 11, 2023
Time: 11:00
Room: Turing 0.E420
Note: This is a training for CPP23

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

[more]
Modernizing the WebDSL Front-End: A Case Study in SDF3 and Statix
Max de Krieger (TU Delft / PL)

Date: Wed, December 21, 2022
Time: 13:00
Room: Lecture Hall F (building 36)
Note: This is a MSc thesis defense

Binary Translation for Weak Memory Model Architectures
Soham Chakraborty (TU Delft / PL)

Date: Wed, December 14, 2022
Time: 12:00
Room: Turing

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.

[more]
Unfolding control for abstract blocks
Jesper Cockx (TU Delft / PL)

Date: Wed, December 07, 2022
Time: 12:00
Room: Turing

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.

[more]
Fencing off unwanted behavior: Improving and evaluating the Fency static analysis tool
Pieter van den Ham (TU Delft / PL)

Date: Fri, December 02, 2022
Time: 15:00
Room: Van der Poelzaal (Building 36)
Note: This is a MSc thesis defense

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)

[more]
Proving functional correctness of monadic programs using separation logic
Liam Clark (TU Delft / PL)

Date: Fri, December 02, 2022
Time: 13:00
Room: t.b.a.
Note: This is a MSc thesis defense

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.

[more]
Formal Methods for Learned Systems
Anna Lukina (TU Delft / Algorithmics)

Date: Wed, November 30, 2022
Time: 12:00
Room: t.b.a.

About Strong and Branching Bisimulation
Jan Friso Groote (TU Eindhoven)

Date: Fri, November 25, 2022
Time: 12:30
Room: Turing 0.E420

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.

[more]
Delft-Utrecht Programming Languages Meeting
t.b.a.

Date: Wed, November 23, 2022
Time: 10:00
Room: t.b.a.

Intrinsically-Typed Definitional Interpreters à la Carte (OOPSLA'22)
Cas van der Rest (TU Delft / PL)

Date: Wed, November 23, 2022
Time: TBA
Room: TBA

This is a SPLASH’22 talk.

[more]
Incremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers (OOPSLA'22)
Aron Zwaan (TU Delft / PL)

Date: Wed, November 23, 2022
Time: TBA
Room: TBA

This is a SPLASH’22 talk.

[more]
Optimising First-Class Pattern Matching (SLE'22)
Jeff Smits (TU Delft / PL)

Date: Wed, November 16, 2022
Time: 11:00
Room: Turing 0.E420 / Zoom

This is a SPLASH’22 talk.

[more]
Language-parametric static semantic code completion (OOPSLA'22)
Daniel A. A. Pelsmaeker (TU Delft / PL)

Date: Wed, November 16, 2022
Time: 11:00
Room: Turing 0.E420 / Zoom

This is a SPLASH’22 talk.

[more]
Specializing Scope Graph Resolution Queries (SLE'22)
Aron Zwaan (TU Delft / PL)

Date: Wed, November 16, 2022
Time: 11:00
Room: Turing 0.E420 / Zoom

This is a SPLASH’22 talk.

[more]
Navigating Through Digital Printing Systems
Bram van Walraven (TU Delft / PL)

Date: Wed, November 09, 2022
Time: 14:00
Room: Snijderszaal building 36 (LB 01.010)
Note: This is a MSc thesis defense

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.

[more]
Towards Automatic Test Suite Generation for Functional Programming Assignments using Budgeted Compositional Symbolic Execution
Wesley Baartman (TU Delft / PL)

Date: Wed, October 26, 2022
Time: 13:00
Room: Lecture Hall D@ta (Building 36 HB.01.630)
Note: This is a MSc thesis defense

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.

[more]
Compiling with Higher-order Effects
Jaro Reinders (TU Delft / PL)

Date: Wed, October 05, 2022
Time: 12:00
Room: Turing 0.E420 / Zoom

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.

[more]
Tactics in Agda using reflection
Paul van der Stel (TU Delft / PL)

Date: Wed, September 21, 2022
Time: 10:00
Room: Snijderszaal LB.01.010 (building 36)
Note: This is a MSc thesis defense

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.

[more]
Extensible elaborators for dependently-typed languages
Bohdan Liesnikov

Date: Wed, September 21, 2022
Time: 12:00
Room: E.420 Turing (building 28) / Zoom room tba

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.

[more]
Stratego 2
Jeff Smits (TU Delft / PL)

Date: Wed, September 14, 2022
Time: 12:00
Room: Turing 0.E420

Session: What did you do last Summer
tba (TU Delft / PL)

Date: Wed, September 07, 2022
Time: 12:00
Room: Turing 0.E420

t.b.a.
Thijs Molendijk (TU Delft / PL)

Date: Tue, August 30, 2022
Time: 17:00
Room: Turing 0.E420 / Zoom t.b.a.
Note: This is a MSc thesis defense

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.

[more]
Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda
Olav de Haas (TU Delft / PL)

Date: Mon, July 11, 2022
Time: 09:00
Room: Snijderszaal (building 36)
Note: This is a MSc thesis defense

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.

[more]
Extending the Domain Specific Language for the Pipelines for Interactive Environments build system
Ivo Wilms (TU Delft / PL)

Date: Fri, July 01, 2022
Time: 10:00
Room: 0.E420 Turing / Ivo's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
Dataflow Analysis in a Language Workbench
Matthijs Bijman (TU Delft / PL)

Date: Wed, June 29, 2022
Time: 15:00
Room: Lecture Hall F (building 36) / Matthijs' Zoom Room
Note: This is a MSc thesis defense

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.

[more]
Function Inlining as a Language Parametric Refactoring
Loek van der Gugten (TU Delft / PL)

Date: Wed, June 22, 2022
Time: 12:00
Room: LB 01.010 Snijderszaal (building 36) / Loek's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
An introduction to Initial Algebra Semantics
Kobe Wullaert (TU Delft / PL)

Date: Wed, June 08, 2022
Time: 12:00
Room: Turing 0.E420

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.

[more]
A Framework for Defining Type Theories
Thiago Felicissimo (Inria, France)

Date: Wed, May 18, 2022
Time: 12:00
Room: Social Data Lab 0.E220

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.

[more]
Describing Inter Parameter Constraints in Web APIs Using Dependent Types
Gerben Oolbekkink (TU Delft / PL)

Date: Tue, May 17, 2022
Time: 15:30
Room: Lecture Hall H (building 36)
Note: This is a MSc thesis defense

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.

[more]
Intrinsically-Typed Language Fragments
Cas van der Rest (TU Delft / PL)

Date: Wed, May 11, 2022
Time: 12:00
Room: Turing 0.E420

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.

[more]
Practice presentation of the paper: Incremental compilation for Stratego
Jeff Smits (TU Delft / PL)

Date: Wed, March 16, 2022
Time: 12:00
Room: Social Data Lab 0.E220

Why is artificial intelligence interested in programming languages?
Sebastijan Dumančić (TU Delft / ALG)

Date: Wed, March 02, 2022
Time: 12:00
Room: Casper's Zoom Room

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.

[more]
Optimising First-Class Pattern Match Compilation
Toine Hartman (TU Delft / PL)

Date: Wed, February 23, 2022
Time: 12:00
Room: Toine's Zoom Room / Social Data Lab 0.E220
Note: This is a MSc thesis defense

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.

[more]
Deriving High-Quality Type-Checkers from Declarative Type-System Specifications
Aron Zwaan (TU Delft / PL)

Date: Wed, January 19, 2022
Time: 11:00
Room: Aron's Zoom Room
Note: This is a PhD Go/No-Go meeting

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.

[more]
Datatype-generic programming and practical subtyping for dependently-typed languages
Lucas Escot (TU Delft / PL)

Date: Wed, January 12, 2022
Time: 11:00
Room: Lucas' Zoom Room
Note: This is a PhD Go/No-Go meeting

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.

[more]
Genetic Program Repair using GHC, QuickCheck & Typed Holes
Leonhard Applis (TU Delft / SERG)

Date: Wed, December 08, 2021
Time: 12:00
Room: Jesper's Zoom room

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

[more]
Deriving Incrementality-Related Program Properties from Scope-Graph-Based Type-Checkers
Aron Zwaan (TU Delft / PL)

Date: Wed, November 24, 2021
Time: 12:00
Room: Aron's Zoom Room

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.

[more]
Typing Extensible Data Types and Functions using Rows
Cas van der Rest (TU Delft / PL)

Date: Wed, November 17, 2021
Time: 12:00
Room: Cas' Zoom Room

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.

[more]
No seminar (SPLASH conference)
t.b.a. (TU Delft / PL)

Date: Wed, October 20, 2021
Time: 12:00
Room: t.b.a.

...
Correct by Construction Language Implementations
Arjen Rouvoet (TU Delft)

Date: Thu, October 14, 2021
Time: 15:00
Room: Senaatszaal, Auditorium
Note: This is a PhD defense. The candidate's talk starts at 14.30.

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.

[more]
No seminar (Arjen's PhD defense on Thursday)
t.b.a. (TU Delft / PL)

Date: Wed, October 13, 2021
Time: 12:00
Room: t.b.a.

Representing variables and scopes for Agda Core
Jesper Cockx (TU Delft / PL)

Date: Wed, October 06, 2021
Time: 12:00
Room: Jesper's zoom room

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.

[more]
Robustness between Weak Memory Models
Soham Chakraborty (TU Delft / PL)

Date: Wed, September 22, 2021
Time: 12:00
Room: Soham's Zoom Room

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.

[more]
Towards a Language for Defining and Composing Languages
Casper Bach Poulsen (TU Delft / PL)

Date: Wed, September 15, 2021
Time: 12:00
Room: Casper's Zoom Room

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.

[more]
Session: What did you do last Summer
Eelco Visser (TU Delft / PL)

Date: Wed, September 01, 2021
Time: 12:00
Room: Eelco's Zoom Room

Incremental Scannerless Generalized LR Parsing
Maarten Sijm (TU Delft / PL)

Date: Wed, July 14, 2021
Time: 10:00
Room: Eelco's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
Towards Principled and Reliable Software System Security
Marco Vassena (CISPA)

Date: Wed, June 30, 2021
Time: 12:00
Room: Eelco's Zoom Room

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?

[more]
A predicate transformer semantics for effects
Wouter Swierstra (Utrecht University)

Date: Wed, June 23, 2021
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Implicit Incremental Type Checking
Aron Zwaan (TU Delft / PL)

Date: Wed, June 16, 2021
Time: 12:00
Room: Aron's Zoom Room

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.

[more]
Verifying Five Haskell Libraries with Agda2Hs
Jesper Cockx (TU Delft / PL)

Date: Wed, June 02, 2021
Time: 12:00
Room: Jesper's Zoom Room

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.

[more]
Renaming for Everyone - Language-parametric Renaming in Spoofax
Phil Misteli (TU Delft / PL)

Date: Tue, May 25, 2021
Time: 14:00
Room: Eelco's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
Compiling with Command Trees
Bernard Bot (TU Delft / PL)

Date: Wed, May 19, 2021
Time: 10:00
Room: Eelco's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
Functional Programming for Big Data Processing
Jan Rellermeyer (TU Delft / Distributed Systems)

Date: Wed, May 12, 2021
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Verifying the Semantics of Disambiguation Rules
Luka Miljak (TU Delft / PL)

Date: Wed, April 28, 2021
Time: 12:00
Room: Eelco's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
Framing Programming Languages: Designing and Using a Frame-Based Virtual Machine
Bram Crielaard (TU Delft / PL)

Date: Wed, April 21, 2021
Time: 10:00
Room: Eelco's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
Testing Consensus Implementations Using Communication Closure
Burcu Kulahcioglu Ozkan (TU Delft / Software Engineering)

Date: Wed, April 07, 2021
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Building a path from language user to sophisticated DSL creator in Racket
Michael Ballantyne (Northeastern University)

Date: Wed, March 31, 2021
Time: 15:00
Room: Eelco's Zoom Room

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.

[more]
A Tour of ML-style module systems
Gabriel Radanne (Inria, France)

Date: Wed, February 24, 2021
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Implementing the Decomposition of Soundness Proofs of Abstract Interpreters in Coq
Jens de Waard (TU Delft / PL)

Date: Wed, February 03, 2021
Time: 12:00
Room: Eelco's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
Composable Type System Specification using Heterogeneous Scope Graphs
Aron Zwaan (TU Delft / PL)

Date: Wed, January 27, 2021
Time: 10:30
Room: Eelco's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
Intrinsically-Typed Language Composition: Go/No-Go
Cas van der Rest (TU Delft / PL)

Date: Wed, January 20, 2021
Time: 12:15
Room: Eelco's Zoom Room
Note: This is a PhD Go/No-Go meeting

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.

[more]
Extracting Agda-embedded DSLs
Artem Shinkarov (Heriot-Watt University)

Date: Wed, January 13, 2021
Time: 12:00
Room: Jesper's Zoom Room

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.

[more]
Paradoxes of probabilistic programming
Jules Jacobs (Radboud University)

Date: Wed, November 25, 2020
Time: 12:00
Room: Jules' Zoom Room

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.

[more]
Staged Effects and Handlers for Modular Languages with Abstraction
Casper Bach Poulsen (TU Delft / PL)

Date: Wed, November 11, 2020
Time: 12:00
Room: Casper's Zoom Room

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.

[more]
Guarded Kleene Algebra with Tests
Tobias Kappé (Cornell University)

Date: Wed, November 04, 2020
Time: 15:20
Room: Zoom

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.

[more]
Relaxed Memory Concurrency and Compiler Correctness
Soham Chakraborty (Indian Institute of Technology Delhi)

Date: Wed, November 04, 2020
Time: 11:05
Room: Zoom

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.

[more]
Speculative Taint Tracking (and a formal analysis of its protection for speculatively-accessed data)
Artem Khyzha (Tel Aviv University)

Date: Wed, October 21, 2020
Time: 11:05
Room: Zoom

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.

[more]
Model-Based Program Verification
Wytse Oortwijn (Eidgenössische Technische Hochschule Zürich)

Date: Wed, October 07, 2020
Time: 11:05
Room: Zoom

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.

[more]
Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
Vladimir Zamdzhiev (Inria, France)

Date: Wed, September 30, 2020
Time: 11:30
Room: Zoom

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.

[more]
A trustworthy and extensible core language for Agda (Veni interview rehearsal)
Jesper Cockx (TU Delft / PL)

Date: Wed, September 09, 2020
Time: 12:00
Room: Jesper's Zoom Room

Opening of the Delft PL Academic Year
(TU Delft / PL)

Date: Wed, September 02, 2020
Time: 12:00
Room: Eelco's Zoom Room

Language Techniques that Enable Higher-levels of Abstraction in Programming
Michael D. Adams (University of Michigan)

Date: Wed, June 24, 2020
Time: 15:00
Room: Eelco's Zoom Room

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.

[more]
Revising Agda's module system
Jesper Cockx (TU Delft / PL)

Date: Wed, June 10, 2020
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Writing plugins and proving them correct in MetaCoq
Bohdan Liesnikov (Saarland University)

Date: Wed, June 03, 2020
Time: 13:00
Room: Eelco's Zoom Room

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.

[more]
Machine-Checked Semantic Session Typing
Jonas Kastberg Hinrichsen (IT University of Copenhagen)

Date: Wed, May 27, 2020
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
A Reconstruction of the Statix Constraint Language
Reuben Rowe (Royal Holloway University of London)

Date: Wed, May 20, 2020
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Getting Things Done
group discussion

Date: Wed, May 13, 2020
Time: 12:00
Room: Eelco's Zoom Room

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

[more]
Dynamix on the Frame VM: Declarative dynamic semantics on a VM using scopes as frames
Chiel Bruin (TU Delft / PL)

Date: Wed, April 29, 2020
Time: 11:00
Room: Eelco's Zoom Room
Note: This is a MSc thesis defense

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.

[more]
A Direct Semantics of Disambiguation by Associativity and Priority Rules
Eelco Visser (TU Delft / PL)

Date: Wed, April 22, 2020
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Early Validation and Global Optimization for Parametric Manufacturing Systems
Jasper Denkers (TU Delft / PL)

Date: Wed, April 15, 2020
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Proving Semantic Type Soundness in Iris
Robbert Krebbers (TU Delft / PL)

Date: Wed, April 08, 2020
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Demo of Intrinsically Typed Compilation of Imperative Code in Agda
Arjen Rouvoet (TU Delft / PL)

Date: Wed, April 01, 2020
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Gradual Types for Stratego - Demo Edition
Jeff Smits (TU Delft / PL)

Date: Wed, March 25, 2020
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Incremental Type Checkers using Scope Graphs
Hendrik van Antwerpen (TU Delft / PL)

Date: Wed, March 18, 2020
Time: 12:00
Room: Eelco's Zoom Room

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.

[more]
Composable, safe-by-construction interpreters for typed languages
Cas van der Rest (TU Delft / PL)

Date: Wed, March 11, 2020
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Reducing the Complexity of Industrial Legacy Software
Arjan Mooij (TNO & TU Delft / PL)

Date: Wed, March 04, 2020
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Univalent Parametricity for Programming Modulo Equivalences
Lucas Escot (École normale supérieure de Lyon)

Date: Wed, February 26, 2020
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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).

[more]
Checking confluence of rewrite rules in Agda
Jesper Cockx (TU Delft / PL)

Date: Wed, February 12, 2020
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Discussion about shoulders of giants: related work in research and writing
Arjen Rouvoet (TU Delft / PL)

Date: Wed, February 05, 2020
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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?
[more]
Redesigning the Spoofax Testing Language
Volker Lanting (TU Delft / PL)

Date: Wed, January 29, 2020
Time: 10:15
Room: Social Data Lab 0.E220
Note: This is a MSc thesis defense

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.

[more]
How to cite a research paper?
Eelco Visser

Date: Wed, January 15, 2020
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.)

[more]
Discussion: How to write a research paper (by Prof. Simon Peyton Jones)

Date: Wed, December 11, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

Integrated (Distributed) Development Environments from Declarative Language Definitions: Go/No-Go
Daniël Pelsmaeker (TU Delft / PL)

Date: Fri, December 06, 2019
Time: 10:30
Room: COLLOQUIUMZAAL 0.E420
Note: This is a PhD go/no-go meeting.

Characterising renaming within OCaml’s module system
Reuben Rowe (Royal Holloway University of London)

Date: Wed, December 04, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Intrinsically-Typed Interpreters for Linear Languages
Arjen Rouvoet (TU Delft / PL)

Date: Wed, November 27, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Compositional Non-Interference for Fine-Grained Concurrent Programs
Dan Frumin (Radboud University Nijmegen)

Date: Wed, November 20, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
...
Language-Parametric Methods for Developing Interactive Programming Systems
Gabriël Konat (TU Delft)

Date: Mon, November 18, 2019
Time: 15:00
Room: Senaatszaal, Auditorium
Note: This is a PhD defense. The candidate's talk starts at 14.30.

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.

[more]
Compiler and Runtime Support for Continuation Marks
Matthew Flatt (University of Utah)

Date: Mon, November 18, 2019
Time: 12:15
Room: Social Data Lab 0.E220

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.

[more]
Incremental Compilers with Internal Build Systems
Jeff Smits (TU Delft / PL)

Date: Mon, November 18, 2019
Time: 11:10
Room: Social Data Lab 0.E220

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.

[more]
Selective Applicative Functors
Andrey Mokhov (Newcastle University)

Date: Mon, November 18, 2019
Time: 10:35
Room: Social Data Lab 0.E220

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.

[more]
Reflections on the Nix build system DSL
Eelco Dolstra (Tweag I/O)

Date: Mon, November 18, 2019
Time: 10:00
Room: Social Data Lab 0.E220

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.

[more]
Symposium Build Systems
Eelco Dolstra, Andrey Mokhov, Jeff Smits, Matthew Flatt, Sebastian Erdweg

Date: Mon, November 18, 2019

Room: EEMCS (building 28), Social Data Lab 0E.220, Van Mourik Broekmanweg 6, 2628 XE Delft
Note: Lunch is served in the room. Please register to attend by sending an email to R.Sharabi@tudelft.nl

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.

[more]
Machine Learning 4 Software Refactoring
Maurício Aniche (TU Delft / Software Engineering)

Date: Wed, November 06, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Hoeveel fouten kun je vinden? Taalgebaseerde softwareveiligheid (in dutch)
Eelco Visser (TU Delft)

Date: Wed, October 30, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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

[more]
From Definitional Interpreter to Symbolic Executor
Casper Bach Poulsen (TU Delft / PL)

Date: Wed, October 16, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Towards an Efficient and Accurate Timing Analysis for Real-Time Cyber-Physical Systems
Mitra Nasri (TU Delft / Ensys)

Date: Wed, October 09, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Generating Constrained Test Data using Datatype Generic Programming
Cas van der Rest (Utrecht University)

Date: Wed, October 09, 2019
Time: 11:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Incrementalizing Statix - A Modular and Incremental Approach for Type Checking and Name Binding using Scope Graphs
Taico Aerts (TU Delft / PL)

Date: Thu, September 26, 2019
Time: 15:00
Room: Social Data Lab 0.E220
Note: This is a MSc thesis defense

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.

[more]
What is PL research?
Eelco Visser (TU Delft / PL)

Date: Wed, September 25, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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

[more]
Session Types and Higher-Order Concurrency
Jorge A. Pérez (University of Groningen)

Date: Wed, September 11, 2019
Time: 12:00
Room: Social Data Lab 0.E220

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.

[more]
Dependent pattern matching: theory and implementation
Jesper Cockx (University of Gothenborg / Chalmers)

Date: Tue, September 10, 2019
Time: 14:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
A type system for dynamic instances
Albert ten Napel (TU Delft / PL)

Date: Thu, September 05, 2019
Time: 14:00
Room: Social Data Lab 0.E220
Note: This is a MSc thesis defense

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.

[more]
Back from Holiday

Date: Wed, September 04, 2019
Time: 12:00
Room: Colloquiumzaal 0.E420

Observability during Bottom Up execution - Improving PIE s change driven incremental build algorithm
Roelof Sol (TU Delft / PL)

Date: Thu, August 29, 2019
Time: 16:00
Room: Social Data Lab 0.E220
Note: This is a MSc thesis defense

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.

[more]
SCL-T - Template programming for Siemens SCL
Jeffrey Goderie (TU Delft / PL)

Date: Thu, August 29, 2019
Time: 12:30
Room: Social Data Lab 0.E220
Note: This is a MSc thesis defense

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.

[more]
Build systems à la carte
Andrey Mokhov (Newcastle University)

Date: Thu, July 04, 2019
Time: 12:00
Room: Social Data Lab 0.E220

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.

[more]
...
Declarative Syntax Definition for Modern Language Workbenches
Eduardo Amorim (TU Delft)

Date: Wed, June 19, 2019
Time: 12:30
Room: Science Centre
Note: This is a PhD defense. The candidate's talk starts at 12:00.

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.

[more]
A Systematic Approach to Static Analysis of Program Transformations
Sebastian Erdweg (Johannes Gutenberg University Mainz)

Date: Tue, June 18, 2019
Time: 17:00
Room: Snijderszaal LB.01.010 (building 36)

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.

[more]
Lambdas Query with Reason
Ralf Lämmel (Facebook London and University of Koblenz-Landau (on leave))

Date: Tue, June 18, 2019
Time: 16:15
Room: Snijderszaal LB.01.010 (building 36)

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.

[more]
Towards Language-Parametric Semantic Editor Services
Daniel Pelsmaeker (TU Delft)

Date: Tue, June 18, 2019
Time: 15:45
Room: Snijderszaal LB.01.010 (building 36)

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.

[more]
A romp through generalised syntax analysis
Elizabeth Scott (Royal Holloway University of London)

Date: Tue, June 18, 2019
Time: 15:00
Room: Snijderszaal LB.01.010 (building 36)

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.

[more]
Monadification of Attribute Grammars
Eric Van Wyk (University of Minnesota)

Date: Tue, June 18, 2019
Time: 14:30
Room: Snijderszaal LB.01.010 (building 36)

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.

[more]
Attribute Grammars: Composable and Modular Language Specifications
Eric Van Wyk (University of Minnesota)

Date: Mon, June 17, 2019
Time: 10:30
Room: Colloquiumzaal 0.E420

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.

[more]
Language Abstractions for Distributed Software Systems
Guido Salvaneschi

Date: Thu, June 06, 2019
Time: 11:00
Room: 0.E220 Social Data Lab

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.

[more]
Deductive Verification for Systems Software
Alex Summers

Date: Thu, June 06, 2019
Time: 09:00
Room: 0.E220 Social Data Lab

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.

[more]
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus von Gleissenthall (University of California)

Date: Fri, May 24, 2019
Time: 09:30
Room: 0.E220 Social Data Lab

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.

[more]
Security Type Error Diagnosis for Functional Languages
Jurriaan Hage (Utrecht University)

Date: Wed, May 22, 2019
Time: 12:00
Room: Lecture Hall L (building 36)

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.

[more]
Brotherston's Conjecture: Equivalence of Inductive Definitions and Cyclic Proofs
Makoto Tatsuta (National Institute of Informatics (NII) Japan)

Date: Mon, May 20, 2019
Time: 12:00
Room: 62-0.15 Lecture Hall F (building 36)

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.

[more]
Frame VM: a virtual machine using scopes as frames
Chiel Bruin (TU Delft)

Date: Wed, May 15, 2019
Time: 12:00
Room: 0.E420 COLLOQUIUMZAAL (Turing)

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.

[more]
Exceptional Asynchronous Session Types: Session Types without Tiers
Simon Fowler (University of Edinburgh)

Date: Wed, May 08, 2019
Time: 11:00
Room: 0.E420 COLLOQUIUMZAAL (Turing)

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.

[more]
Implementing the Decomposition of Soundness Proofs of Abstract Interpreters in Coq
Jens de Waard (TU Delft PL)

Date: Wed, May 01, 2019
Time: 12:00
Room: 0.E420 COLLOQUIUMZAAL

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.

[more]
Generalised parsing with binary subtree representations
Thomas van Binsbergen (Royal Holloway University)

Date: Wed, April 24, 2019
Time: 12:00
Room: 0.E420 COLLOQUIUMZAAL

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.

[more]
Building a Foundation for Verification of Distributed Systems in Iris
Jonas Kastberg Hinrichsen (IT University of Copenhagen)

Date: Thu, April 11, 2019
Time: 15:00
Room: 0.E420 COLLOQUIUMZAAL

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.

[more]
Semi-Automated Reasoning About Non-Determinism in C Expressions
Léon Gondelman (Radboud University Nijmegen)

Date: Wed, April 03, 2019
Time: 12:00
Room: 0.E420 COLLOQUIUMZAAL

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.

[more]
Enforcing C-level security policies using machine-level tags
Andrew Tolmach (Portland State University)

Date: Wed, April 03, 2019
Time: 11:00
Room: 0.E420 COLLOQUIUMZAAL

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.

[more]
...
Modeling at Scale: Go/No-Go
Jasper Denkers (TU Delft PL)

Date: Thu, March 28, 2019
Time: 720.0
Room: 0.E220 Social Data Lab
Note: This is a PhD go/no-go meeting.

...
Distributed programming using role-parametric session types in Go
Sung-Shik Jongmans (Open University)

Date: Wed, March 27, 2019

Room: 0.E420 COLLOQUIUMZAAL (Turing)

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.

[more]
...
Declarative Specification of Information System Data Models and Business Logic
Daco Harkes (TU Delft, Google)

Date: Tue, March 26, 2019

Room: Aula Conference Centre (building 20), Mekelweg 5, 2628 CC Delft
Note: This is a PhD defense. The candidate's talk starts at 14:30.

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.

[more]
Towards Language-Parametric Semantic Editor Services based on Declarative Type System Specifications
Hendrik van Antwerpen (TU Delft)

Date: Tue, March 26, 2019

Room: EEMCS (building 36), Snijderszaal LB 01.010, Mekelweg 4, 2628 CD Delft

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.

[more]
...
Relations in JastAdd
Görel Hedin (Lund University)

Date: Tue, March 26, 2019

Room: EEMCS (building 36), Snijderszaal LB 01.010, Mekelweg 4, 2628 CD Delft

ACID for Programmers
Friedrich Steimann (FernUniversität in Hagen)

Date: Tue, March 26, 2019

Room: EEMCS (building 36), Snijderszaal LB 01.010, Mekelweg 4, 2628 CD Delft

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.

[more]
Distributed system development with ScalaLoci
Guido Salvaneschi (TU Darmstadt)

Date: Tue, March 26, 2019

Room: EEMCS (building 36), Snijderszaal LB 01.010, Mekelweg 4, 2628 CD Delft

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.

[more]
Symposium Declarative Programming
Görel Hedin, Friedrich Steimann, Guido Salvaneschi, Hendrik van Antwerpen

Date: Tue, March 26, 2019

Room: EEMCS (building 36), Snijderszaal LB 01.010, Mekelweg 4, 2628 CD Delft
Note: The symposium is followed by lunch served in the room. Please register to attend by sending an email to R.Sharabi@tudelft.nl

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.

[more]
Reuse and co-evolution in CBS language specifications
Peter Mosses (TU Delft PL)

Date: Wed, March 20, 2019
Time: 720.0
Room: 0.E420 COLLOQUIUMZAAL (Turing)

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.

[more]
A Direct Semantics for Declarative Disambiguation of Expression Grammars
Eelco Visser (TU Delft)

Date: Wed, March 13, 2019

Room: 0.E420 COLLOQUIUMZAAL (Turing)

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.

[more]
Terminating Type System in Iris
Guillaume Ambal (ENS)

Date: Wed, March 06, 2019
Time: 11:00
Room: TBA

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.

[more]
The Constraint Programming Language MiniZinc
Neil Yorke-Smith (TU Delft Algorithms Group)

Date: Wed, March 06, 2019

Room: 0.E420 COLLOQUIUMZAAL (Turing)

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

[more]
Towards Semantic Type Soundness for Dependent Object Types and Scala with Logical Relations in Iris
Paolo Giarrusso (EPFL)

Date: Wed, February 13, 2019
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Dependent Types for Invariants in Session Types
Wiebe van Geest (TU Delft / PL)

Date: Fri, December 14, 2018
Time: 10:30
Room: Snijderszaal LB.01.010 (building 36)
Note: This is a MSc thesis defense

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.

[more]
Conformance Testing as a Tool for Designing Connected Vehicle Functions
Mohammad Reza Mousavi (University of Leicester)

Date: Thu, December 13, 2018
Time: 12:00
Room: Social Data Lab 0.E220

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.

[more]
Testing Code Generators against Definitional Interpreters
Ioannis Papadopoulos (TU Delft / PL)

Date: Wed, December 05, 2018
Time: 11:45
Room: Prisma (Bouwcampus)
Note: This is a MSc thesis defense

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.

[more]
Using Z3 with 900 first-year students
Sebastian Erdweg (TU Delft / PL)

Date: Wed, November 21, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Should we leave C behind us?
Erwin Gribnau (Technolution)

Date: Wed, November 14, 2018
Time: 12:00
Room: Social Data Lab 0.E220

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.

[more]
Incremental Type Checking in IncA
Sander Bosma (TU Delft / PL)

Date: Fri, November 02, 2018
Time: 11:00
Room: Snijderszaal LB.01.010 (building 36)
Note: This is a MSc thesis defense

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.

[more]
Abstract Interpretation of Program Transformations using Regular Tree Grammars
Jente Hidskes (TU Delft / PL)

Date: Fri, November 02, 2018
Time: 09:00
Room: Snijderszaal LB.01.010 (building 36)
Note: This is a MSc thesis defense

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.

[more]
Incrementalizing Lattice-Based Program Analyses in Datalog
Tamás Szabó (TU Delft / PL)

Date: Thu, November 01, 2018
Time: 12:00
Room: Dijkstrazaal HB09.150 (building 36)

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

[more]
Scopes as Types
Hendrik van Antwerpen (TU Delft / PL)

Date: Thu, November 01, 2018
Time: 12:30
Room: Dijkstrazaal HB09.150 (building 36)

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

[more]
Migrating Custom DSL Implementations to a Language Workbench (Tool Demo)
Jasper Denkers (TU Delft / PL)

Date: Wed, October 24, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Language specification using funcons
Peter Mosses (TU Delft / PL)

Date: Wed, October 17, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Abstractions for Transformations
Eelco Visser (TU Delft / PL)

Date: Wed, October 10, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Scopes as Types
Hendrik van Antwerpen (TU Delft / PL)

Date: Wed, September 26, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Compositional soundness proofs of abstract interpreters
Sven Keidel (TU Delft / PL)

Date: Wed, September 19, 2018
Time: 12:30
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
MoSeL - A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
Robbert Krebbers (TU Delft / PL)

Date: Wed, September 19, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Scalable Incremental Building with Dynamic Task Dependencies
Gabriël Konat (TU Delft / PL)

Date: Wed, August 29, 2018
Time: 12:00
Room: Hilbert 2.W510

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.

[more]
Relations for Incremental Verification
Sebastiaan Joosten (University of Twente)

Date: Wed, August 22, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Towards Language Parametric Web-Based Development Environments
Olaf Maas (TU Delft / PL)

Date: Fri, July 13, 2018
Time: 13:00
Room: Snijderszaal LB 01.010 (building 36)
Note: This is a MSc thesis defense

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.

[more]
Better living through incrementality - Immediate static analysis feedback without loss of precision
Sebastian Erdweg (TU Delft / PL)

Date: Wed, June 20, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
ReLoC - A Mechanised Relational Logic for Fine-Grained Concurrency
Dan Frumin (Radboud University Nijmegen)

Date: Wed, June 13, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Mtac2 - Typed Tactics for Backward Reasoning in Coq
Robbert Krebbers (TU Delft / PL)

Date: Wed, June 06, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
Statix - Typechecking with Scope Graphs and Constraints
Hendrik van Antwerpen (TU Delft / PL)

Date: Wed, May 30, 2018
Time: 12:00
Room: HG.2.66 (Faculty of CEG)

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.

[more]
Aim, Relevance, Methods, Results, and Evidence in IceDust Research
Daco Harkes (TU Delft / PL)

Date: Wed, May 23, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
To-Many or To-One? All-in-One! Efficient Purely Functional Multi-maps with Type-Heterogeneous Hash-Tries
Michael Steindorfer (TU Delft / PL)

Date: Wed, May 16, 2018
Time: 12:00
Room: Hilbert 2.W510

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.

[more]
Testing Code Generators against Definitional Interpreters
Ioannis Papadopoulos (TU Delft)

Date: Wed, May 09, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

PART I Testing Code Generators against Definitional Interpreters

[more]
Portable Editor Services
Daniël Pelsmaeker (TU Delft / PL)

Date: Thu, May 03, 2018
Time: 14:00
Room: Snijderszaal LB 01.010 (building 36)
Note: This is a MSc thesis defense

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?

[more]
Compositional Soundness Proofs of Abstract Interpreters
Sven Keidel (TU Delft / PL)

Date: Wed, May 02, 2018
Time: 12:00
Room: COLLOQUIUMZAAL 0.E420

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.

[more]
The Design and Implementation of a Domain-Specific Language for the Description of Medical Devices
Tim Rensen (TU Delft / PL)

Date: Wed, April 18, 2018
Time: 15:00
Room: Lecture Hall D@ta (building 36)
Note: This is a MSc thesis defense

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.

[more]
Random Term Generation for Compiler Testing in Spoofax
Martijn Dwars (TU Delft / PL)

Date: Tue, April 03, 2018
Time: 09:00
Room: Lecture Hall L (building 36)
Note: This is a MSc thesis defense

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.

[more]
Building a Unified Call Graph at Ecosystem Level
Joseph Hejderup (TU Delft / Software Engineering)

Date: Wed, March 28, 2018
Time: 12:00
Room: HG.2.66 (Faculty of CEG)

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.

[more]
Towards Zero-Overhead Disambiguation of Deep Priority Conflicts
Eduardo de Souza Amorim (TU Delft / PL)

Date: Wed, March 21, 2018
Time: 12:00
Room: Yellow Brickroad (Bouwcampus)

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.

[more]
Good Scientific Practice
Sebastian Erdweg (TU Delft / PL)

Date: Wed, March 14, 2018
Time: 12:00
Room: HG.2.66 (Faculty of CEG)

“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]

[more]
Getting Spoofax To The Web - Client-Side Language Execution
Olaf Maas (TU Delft / PL)

Date: Wed, March 07, 2018
Time: 12:00
Room: Yellow Brickroad (Bouwcampus)

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.

[more]
Type-Directed Diffing of Structured Data
Victor Miraldo (Utrecht University)

Date: Wed, February 28, 2018
Time: 12:00
Room: Yellow Brickroad (Bouwcampus)

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.

[more]
Statix - A Language for Static Semantics
Hendrik van Antwerpen (TU Delft / PL)

Date: Wed, February 21, 2018
Time: 12:00
Room: HG.2.66 (Faculty of CEG)

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.

[more]
Dependent Types for Invariants in Session Types
Wiebe van Geest (TU Delft / PL)

Date: Wed, February 14, 2018
Time: 12:00
Room: HG.2.62 (Faculty of CEG)

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.

[more]
Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic
Robbert Krebbers (TU Delft / PL)

Date: Wed, February 07, 2018
Time: 12:00
Room: Yellow Brickroad (Bouwcampus)

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.

[more]
Dynamic instances for algebraic effects and handlers
Albert ten Napel (TU Delft / PL)

Date: Wed, January 31, 2018
Time: 12:45
Room: Yellow Brickroad (Bouwcampus)

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.

[more]
IncA case study - implementing a type checker for the Rust language
Sander Bosma (TU Delft / PL)

Date: Wed, January 31, 2018
Time: 12:30
Room: Yellow Brickroad (Bouwcampus)

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.

[more]
Increasing precision of Abstract Interpretation of Program Transformations
Jente Hidskes (TU Delft / PL)

Date: Wed, January 31, 2018
Time: 12:15
Room: Yellow Brickroad (Bouwcampus)

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.

[more]
Implementing Rust borrow checking with Spoofax
Amin Ait Lamqadem (Università di Pisa)

Date: Wed, January 31, 2018
Time: 12:00
Room: Yellow Brickroad (Bouwcampus)

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.

[more]
A Modular SGLR Parsing Architecture for Systematic Performance Optimization
Jasper Denkers (TU Delft / PL)

Date: Wed, January 24, 2018
Time: 11:00
Room: Hall Chip (building 36)
Note: This is a MSc thesis defense

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.

[more]
Incrementalizing Lattice-Based Program Analyses
Tamás Szabó (TU Delft / PL)

Date: Wed, January 17, 2018
Time: 12:00
Room: Snijderszaal LB.01.010 (building 36)

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.

[more]
...
Generic Tools, Specific Languages
Markus Voelter (TU Delft)

Date: Wed, June 18, 2014
Time: 12:30
Room: Aula Conference Centre (building 20)

Reference

[more]
...
Methods and Techniques for the Design and Implementation of Domain-Specific Languages
Zef Hemel (TU Delft)

Date: Wed, January 11, 2012
Time: 12:30
Room: Aula Conference Centre (building 20)

Reference

[more]
...
Building Blocks For Language Workbenches
Lennart Kats (TU Delft)

Date: Tue, December 13, 2011
Time: 15:00
Room: Aula Conference Centre (building 20)

Reference

[more]