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

13:30 - 15:10: PLNL - 2 at Boothzaal
Chair(s): Wouter SwierstraUtrecht University, Netherlands
plnl-2018-papers13:30 - 13:55
plnl-2018-papers13:55 - 14:20
Casper Bach PoulsenDelft University of Technology
plnl-2018-papers14:20 - 14:45
Mart LubbersRadboud University Nijmegen, Pieter KoopmanRadboud University Nijmegen, Netherlands, Rinus PlasmeijerRadboud University Nijmegen
plnl-2018-papers14:45 - 15:10
Manuel ChakravartyTweag I/O & IOHK