The programme arises as the combination of the LFMTP and MLPA programmes and of invited and contributed presentations.
We will organize a common, informal dinner for interested participants at the conclusion of the workshop. Lunch and coffee breaks (but not the dinner) are covered by the workshop registration.

Session 1

9:00 - 9:30      Henk Barendregt

                       Accepting formalized proofs

9:30 - 10:10    Aleksandar Nanevski

                       How to make ad hoc proof automation less ad hoc

Coffee Break

Session 2

10:30 - 11:10  Michael Norrish

                       Syntax: Getting over it already?

11:10 - 11:50  Mathieu Boespflug and Brigitte Pientka

                       Multi-level Contextual Type Theory

11:50 - 12:30  Alan J. Martin and Amy Felty

                       An Improved Implementation and Abstract Interface for Hybrid

Lunch Break

Session 3

14:00 - 14:40  Derek Dreyer

                       MixML Remixed

14:40 - 15:20  Andreas Abel and Nicolai Kraus

                       A Lambda Term Representation Based on Linear Ordered Logic

15:20 - 16:00  Maxime Beauquier and Carsten Schuermann

                       A Bigraph Relational Model

Coffee Break

Session 4

16:30 - 17:10  Ranald Clouston

                       Nominal Logic with Equations Only

17:10 - 17:50  Murdoch Gabbay and Dominic Mulligan

                       Nominal semantics of simply-typed lambda-calculus

17:50 - 18:30  Jesse Alama

                       Generalizing Theorems of the Mizar Mathematical Library by Type Promotion and Property Omission

18:30 - 18:40  Closing Remarks