Invited Talks

• Markus Püschel (ETH Zürich, Switzerland): Compiling Math to High Performance Code
  
  

• Martin Berger (University of Sussex, UK): Specification and verification of meta-programs
  
  Abstract: This lecture outlines key approaches to meta-programming (MP), and introduces the nascent work on verification of meta-programs. We begin by clarifying terminology: we compare and contrast the main forms of modern MP languages: compile-time MP (as can be found in Template Haskell or Converge), run-time MP (as provided by the MetaML^? family of languages), and printf-based MP (used in languages that do not offer dedicated MP features). Next we outline the existing approaches to typing MP, which can be done statically (e.g. the MetaML^? family of languages), or dynamically (e.g. Converge), or in hybrid form (e.g. Template Haskell). Then we introduce a program logic for an idealised MP language, and use it to demonstrate reasoning about small meta-programs. We also discuss how logics for non MP-languages can be used as heuristics for constructing logics for MP languages. Next we look at logics for languages featuring a Javascript-like eval construct. Finally, we sketch recent alternative approaches to reasoning about the correctness of MP based on the Curry-Howard correspondence, on translation of MP-languages into non-MP-languages, and on equational reasoning. We conclude by suggesting interesting questions for future work, including the quest for a Church-Turing thesis for MP.