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

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 (EEMCS 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]
TBA
TBA (TBA)

Date: Wed, May 22, 2019
Time: 12:00
Room: TBA

TBA
TBA

Date: Wed, June 05, 2019
Time: 12:00
Room: TBA

Attribute Grammars
Eric Van Wyk

Date: Wed, June 12, 2019
Time: 11:00
Room: TBA

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 com- puter 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 imple- mentation.

[more]
TBA
TBA

Date: Wed, June 26, 2019
Time: 12:00
Room: TBA

Build systems à la carte
Andrey Mokhov (Newcastle University)

Date: Thu, July 04, 2019
Time: 12:00
Room: TBA

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]
TBA (reserved)
TBA

Date: Fri, July 12, 2019
Time: 12:00
Room: TBA

PL Seminar goes on Summer Break
TBA

Date: Wed, July 17, 2019
Time: 12:00
Room: TBA

Opening of the Academic Year
TBA

Date: Wed, September 04, 2019
Time: 12:00
Room: TBA

Past Talks

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: 660.0
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

Room: 0.E420 COLLOQUIUMZAAL (Turing)

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]