Second International Summer School on Metaprogramming
Metaprogramming is an approach to improving programs by treating program fragments (such as expressions or types) as values that the program can manipulate. Metaprogramming comes in various forms, including
- staged programming: treating expressions as program values.
The execution of a staged program is spread over several phases, with each stage using the available data to generate specialized code.
Staged programming has a wide variety of applications — numeric computations, parsing, database queries, generic programming, domain specific languages, and many more. Precompiling the staged code can have dramatic performance improvements, in some cases an order of magnitude or more.
- generic programming: treating types as program values.
Generic programming can improve code flexibility, allowing to give a single definition of a function that operates in a predictable (but not uniform) way on many different types.
Generic programming techniques can be used to define a wide variety of functions, including traversals, comparisons, pretty printers, serialization functions, and many more.
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 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/
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.
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.
See the application page for details.
- 30 June: Application and reference letters deadline.
- 10 July: Notification of acceptance.
- 11 August: Summer school.
Fees70 Euros / day (includes full board and accommodation)
Previous eventsFirst International Summer School on Metaprogramming (Cambridge, 2016)
OrganisersYukiyoshi Kameyama (University of Tsukuba)
Ohad Kammar (University of Edinburgh)
Jeremy Yallop (University of Cambridge)