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

What is PL research?
Eelco Visser (TUDelft / 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]
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

TBA
TBA

Date: Wed, October 02, 2019
Time: 12:00
Room: TBA

TBA
Mitra Nasri (TUDelft)

Date: Wed, October 09, 2019
Time: 12:00
Room: TBA

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

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

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]

Past Talks

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

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

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

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

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

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

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

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

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

[more]
Back from Holiday

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Editor services assist programmers to more effectively write and comprehend code. Implementing editor services correctly is not trivial. This presentation focuses on our paper, which discusses the specification of semantic editor services, those that use the semantic model of a program. The specification of refactorings is a common subject of study, but many other semantic editor services have received little attention. We propose a language-parametric approach to the definition of semantic editor services, using a declarative specification of the static semantics of the programming language, and constraint solving. Editor services are specified as constraint problems, and language specifications are used to ensure correctness. We describe our approach for the following semantic editor services: reference resolution, find usages, goto subclasses, code completion, and the extract definition refactoring. We do this in the context of Statix, a constraint language for the specification of type systems. We investigate the specification of editor services in terms of Statix constraints, and the requirements these impose on a suitable solver.

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

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

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

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

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

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

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

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

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

[more]
Language Abstractions for Distributed Software Systems
Guido Salvaneschi

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

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

[more]
Deductive Verification for Systems Software
Alex Summers

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[more]
Building a Foundation for Verification of Distributed Systems in Iris
Jonas Kastberg

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

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

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

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

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

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

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

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

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

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

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

Date: Wed, March 27, 2019

Room: 0.E420 COLLOQUIUMZAAL (Turing)

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

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

Date: Tue, March 26, 2019

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

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

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

Date: Tue, March 26, 2019

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

Editor services assist programmers to more effectively write and comprehend code. Implementing editor services correctly is not trivial. This paper focuses on the specification of semantics editor services, those that use the semantic model of a program. The specification of refactorings is a common subject of study, but many other semantics editor services have received little attention.

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

Date: Tue, March 26, 2019

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

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

Date: Tue, March 26, 2019

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

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

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

Date: Tue, March 26, 2019

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

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

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

Date: Tue, March 26, 2019

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

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

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

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

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

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

Date: Wed, March 13, 2019

Room: 0.E420 COLLOQUIUMZAAL (Turing)

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

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

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

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

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

Date: Wed, March 06, 2019

Room: 0.E420 COLLOQUIUMZAAL (Turing)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

PART I Testing Code Generators against Definitional Interpreters

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[more]