Second International Summer School on Metaprogramming

Schloss Dagstuhl, 11^th to 16^th August 2019

About

Metaprogramming is an approach to constructing programs by treating program fragments (such as expressions or types) as values that the program can manipulate. Metaprogramming comes in various forms — for example,

in dependently-typed programming terms appear within types, supporting the construction of precise specifications of functions and data.
in multi-stage programming expressions are program values, making it possible to write safe program generation programs that can significantly improve performance.
in languages with macros programs execute partly during compilation and partly at run-time, eliminating the sharp distinction between built-in and user-defined constructs.
embedded domain-specific languages reuse host language features such as syntax and type-checking for convenient definition of little languages suited to a particular endeavour.

Metaprogramming has many applications, including genericity, proof automation, language extensibility and user-defined optimization.

The goal of the summer school is to explore the state-of-the art in metaprogramming and its applications, covering both theory and practice.

Lecturers and courses

Oleg Kiselyov (Tohoku University)

on From the tagless-final cookbook: simple hardware description language and optimization-by-evaluation

Oleg Kiselyov is an Assistant Professor at the Graduate School of Information Sciences at Tohoku University, Japan. More information is on the web site http://okmij.org/ftp/

Matthew Flatt (University of Utah)

on Building Languages with Racket

Matthew Flatt is a professor in the School of Computing at the University of Utah, where he works on extensible programming languages, run-time systems, and applications of functional programming. He is one of the developers of the Racket programming language.

Conor McBride (University of Strathclyde)

on Exploring Universes

Conor McBride is a Reader in the Mathematically Structured Programming group at the University of Strathclyde. He completed of his PhD at the University of Edinburgh in 1999, working on dependently-typed programming when the functional programming community was highly suspicious of it. He has spent the last twenty years having rather too much fun, so now they are suspicious for different reasons.

Jonathan Protzenko (Microsoft Research Redmond)

on Meta-F*: efficient meta-programming of the F* compiler at every stage

I am a Researcher in the RiSE group at Microsoft Research in Redmond. My research interests lie at the intersection of programming languages, type systems, software verification and security. My main area of focus is the design, implementation and evolution of Low*, a low-level subset of F* which compiles to C or WebAssembly. I contribute to or drive several projects that make use of Low* and its dedicated compiler KreMLin, such as the HACL* cryptographic library (used in Firefox, the Tezos blockchain), the EverCrypt cryptographic provider (used in Windows, mbedTLS) and Signal*, a verified implementation of the Signal protocol that compiles to WebAssembly. I am a member of Project Everest, an ambitious joint research effort between Microsoft Research, INRIA, CMU and the University of Edinburgh that aims to write and deploy a verified HTTPS stack.

Supernumerary lecture by Jamie Gabbay (Heriot-Watt University)

on Programming with nominal techniques

Jamie Gabbay studies mathematical foundations and their applications to programming and computer science. He got a PhD in mathematical computer science from Cambridge University in 2001. After several postdocs including in the Ecole Polytechnique in Paris France and the TU/e in the Netherlands, he got a lectureship in Heriot-Watt University in Edinburgh. Most recently, he has been consulting with IOHK. In 2019 he was awarded the LICS "Test of time" award and the EATCS Church Award for Outstanding Contributions to Logic and Computation.

Prerequisites

The school is aimed at graduate students in programming languages and related areas, but is open to researchers, practitioners and strong masters students with the support of a supervisor. Some experience of typed functional programming in Haskell, OCaml, Scala, or a similar language will be assumed.

Registration

See the application page for details.

Application timetable

30 June: Application and reference letters deadline.
10 July: Notification of acceptance.
11 August: Summer school.

Fees

70 Euros / day (includes full board and accommodation)

Previous events

First International Summer School on Metaprogramming (Cambridge, 2016)

Organisers

Yukiyoshi Kameyama (University of Tsukuba)
Ohad Kammar (University of Edinburgh)
Jeremy Yallop (University of Cambridge)