Write a Blog >>
Thu 22 Nov 2018 13:55 - 14:20 at Boothzaal - 2 Chair(s): Wouter Swierstra

Definitional interpreters are an approach to specifying the semantics of an object language by implementing an interpreter in a meta language. The approach is attractive because it supports clear and concise specifications that are validatable-by-construction through execution. If we use a dependently typed meta language we seemingly get even more benefits: we can write intrinsically typed interpreters that are safe-by-construction, thereby alleviating the need for tedious and manual type soundness proofs. But implementing intrinsically typed interpreters is challenging. Data structures must be engineered to allow dependently typed host languages to infer their safe usage. And language extensions may require subtle and far reaching modifications. Furthermore, since intrinsically typed interpreters operate on intrinsically typed syntax, specification validatability is dependent on either manually constructing a well-typedness proof for each input program, or on writing a type checker that does it for us. This talk will summarize recent advances towards scaling intrinsically typed interpreters to object languages with imperative features, and discuss open problems with supporting language evolution and scaling the approach to even more object languages.

Thu 22 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:10
2PLNL at Boothzaal
Chair(s): Wouter Swierstra Utrecht University, Netherlands
13:30
25m
Talk
From Rascal to JVM byte code: a play in several acts
PLNL
13:55
25m
Talk
Intrinsically Typed Definitional Interpreters: The Good, The Bad, and The Ugly
PLNL
Casper Bach Poulsen Delft University of Technology
14:20
25m
Talk
Task Oriented Programming for the Internet of Things
PLNL
Mart Lubbers Radboud University Nijmegen, Pieter Koopman Radboud University Nijmegen, Netherlands, Rinus Plasmeijer Radboud University Nijmegen
14:45
25m
Talk
A Functional Approach to Blockchain Contract Languages
PLNL
Manuel Chakravarty Tweag I/O & IOHK