Intrinsically Typed Definitional Interpreters: The Good, The Bad, and The Ugly
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 NovDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:10 | |||
13:30 25mTalk | From Rascal to JVM byte code: a play in several acts PLNL | ||
13:55 25mTalk | Intrinsically Typed Definitional Interpreters: The Good, The Bad, and The Ugly PLNL Casper Bach Poulsen Delft University of Technology | ||
14:20 25mTalk | 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 25mTalk | A Functional Approach to Blockchain Contract Languages PLNL Manuel Chakravarty Tweag I/O & IOHK |