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
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
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
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
Dinner