## 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

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

## Past Talks

##### 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]
##### Tba
###### tba

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

##### 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

[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]
###### 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]
###### 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

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

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

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

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

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

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

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

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

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

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]