I created a YouTube playlist with recordings of talks by members of the TU Delft Programming Languages group. (Let me know if I missed any.)

Talk by Arjen Rouvoet at POPL 2018 about our paper:

Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser. Intrinsically-typed definitional interpreters for imperative languages, PACM PL (POPL 18)

Abstract: A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a separate type system requires a separate type safety proof. An alternative approach, at least for pure object languages, is to use a dependently-typed language to encode the object language type system in the definition of the abstract syntax. Using such intrinsically-typed abstract syntax definitions allows the host language type checker to verify automatically that the interpreter satisfies type safety. Does this approach scale to larger and more realistic object languages, and in particular to languages with mutable state and objects?

In this paper, we describe and demonstrate techniques and libraries in Agda that successfully scale up intrinsically-typed definitional interpreters to handle rich object languages with non-trivial binding structures and mutable state. While the resulting interpreters are certainly more complex than the simply-typed lambda-calculus interpreter we start with, we claim that they still meet the goals of being concise, comprehensible, and executable, while guaranteeing type safety for more elaborate object languages. We make the following contributions: (1) A dependent-passing style technique for hiding the weakening of indexed values as they propagate through monadic code. (2) An Agda library for programming with scope graphs and frames, which provides a uniform approach to dealing with name binding in intrinsically-typed interpreters. (3) Case studies of intrinsically-typed definitional interpreters for the simply-typed lambda-calculus with references (STLC+Ref) and for a large subset of Middleweight Java (MJ).

Code: https://metaborg.github.io/mj.agda/

TU Delft Programming Languages Group

The TU Delft Programming Languages group on December 13, 2017

  • Daniël Pelsmaeker
  • Jasper Denkers
  • Olaf Maas
  • Wiebe van Geest
  • Albert ten Napel
  • Sebastian Erdweg
  • Casper Bach Poulsen
  • Elmer van Chastelet
  • Jeff Smits
  • Michael Steindorfer
  • Danny Groenewegen
  • Nick ten Veen
  • Daco Harkes
  • Sven Keidel
  • Eduardo Amorim
  • Gabriël Konat
  • Arjen Rouvoet
  • Ioannis Papadopoulos
  • Robbert Krebbers
  • Peter Mosses
  • Sander Bosma
  • Jente Hidskes
  • Hendrik van Antwerpen
  • Eelco Visser

more group pictures

Talk by Jeff Smits about the paper:

Jeff Smits, Eelco Visser. FlowSpec: declarative dataflow analysis specification. In Benoît Combemale, Marjan Mernik, Bernhard Rumpe, editors, Proceedings of the 10th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2017, Vancouver, BC, Canada, October 23-24, 2017. pages 221-231, ACM, 2017. [doi] [researchr]

Abstract: We present FlowSpec, a declarative specification language for the domain of dataflow analysis. FlowSpec has declarative support for the specification of control flow graphs of programming languages, and dataflow analyses on these control flow graphs. We define the formal semantics of FlowSpec, which is rooted in Monotone Frameworks. We also discuss a prototype implementation of the language, built in the Spoofax Language Workbench. Finally, we evaluate the expressiveness and conciseness of the language with two case studies. These case studies are analyses for Green-Marl, an industrial, domain-specific language for graph processing. The first case study is a classical dataflow analysis, scaled to this full language. The second case study is a domain-specific analysis of Green-Marl.

Talk by Daco Harkes at ECOOP 2017 about the paper:

Daco Harkes, Eelco Visser. IceDust 2: Derived Bidirectional Relations and Calculation Strategy Composition. In Peter Müller 0001, editor, 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain. Volume 74 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. [doi] [PDF]

Abstract: Derived values are values calculated from base values. They can be expressed with views in relational databases, or with expressions in incremental or reactive programming. However, relational views do not provide multiplicity bounds, and incremental and reactive programming require significant boilerplate code in order to encode bidirectional derived values. Moreover, the composition of various strategies for calculating derived values is either disallowed, or not checked for producing derived values which will be consistent with the derived values they depend upon. In this paper we present IceDust2, an extension of the declarative data modeling language IceDust with derived bidirectional relations with multiplicity bounds and support for statically checked composition of calculation strategies. Derived bidirectional relations, multiplicity bounds, and calculation strategies all influence runtime behavior of changes to data, leading to hundreds of possible behavior definitions. IceDust2 uses a product-line based code generator to avoid explicitly defining all possible combinations, making it easier to reason about correctness. The type system allows only sound composition of strategies and guarantees multiplicity bounds. Finally, our case studies validate the usability of IceDust2 in applications.