Second International Summer School on Metaprogramming

Preparation: software to install

• Racket
  In addition to DrRacket, you should install the "plait' package.
  You can use DrRacket's "Install Package" menu item under "File" with the package name "plait".
• Agda 2.6.0.1
• OCaml
• (more to follow)

Building Languages with Racket

Matthew Flatt (University of Utah)

• Lecture notes: Building Languages with Racket

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

Jonathan Protzenko (Microsoft Research)

• Slides: F* and Meta-F*: Formal Verification, Language Extensibility, and Proof automation
• Files:
  • Live.fst
  • TypeClass.fst
  • FStar.Tactics.Canon.fst
  • FStar.Tactics.CanonCommSemiring.fst
• Labs:
  • for students who are new to F*, please follow the online tutorial
  • for students who are familiar with F* and have F* installed locally (see INSTALL.md) along with the Emacs fstar-mode, please complete these exercises:
    • Intro.fst
    • Automation.fst
    • Hybrid.fst
    • Metaprogramming.fst
    • Constructive.fst
    • Term.fst

Exploring Universes

Conor McBride (University of Strathclyde)

• Repository: ProgrammerCommaCon

Programming with nominal techniques

Jamie Gabbay (University of Strathclyde)

• Slides: Programming with Nominal Techniques
• Nominal_IOref.hs
• Nominal_resumable_exceptions.hs
• SystemF.hs

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

Oleg Kiselyov (Tohoku University, Japan)

• Slides: From the tagless-final cookbook: simple hardware description language and optimization-by-evaluation
• algebra.ml
• basic_gates.ml
• bconst_prop.ml
• nand.ml
• bneg_adhoc.ml
• cnf.ml
• circuit.ml

Steps towards structured multi-stage programming

Jeremy Yallop (University of Cambridge)

• Slides: Multi-stage programming, part one: static vs dynamic
• Files: recursion.ml, strings.ml