We are proud to present the following two invited talks:

• Markus Püschel (ETH Zürich, Switzerland): Compiling Math to High Performance Code
  
  Abstract Extracting optimal performance from modern computing platforms has become increasingly difficult over the last few years. The effect is particularly noticeable in computations that are of mathematical nature such as those needed in multimedia processing, communication, control, graphics, and scientific simulations. The reason is in optimizations that are known to be difficult and often impossible for compilers: parallelization, vectorization, and locality optimizations. On the other hand, many mathematical applications spend most of their runtime in well-defined mathematical kernels such as matrix computations, Fourier transforms, interpolation, coding, and others. Since these are likely to be needed for decades to come, it makes sense to build program generation systems for their automatic production. With Spiral we have built such a system for the domain of linear transforms. In this talk we give a brief survey on the key techniques underlying Spiral: a domain specific mathematical language, rewriting systems for different forms of parallelization and to compute the so-called recursion step closure to improve locality in recursive code, and the use of machine learning to adapt code at installation time. Spiral-generated code has proven to be as good as, and sometimes faster, than any human-written 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.