The LFMTP 2011 workshop will be held jointly with the MLPA 2011 workshop. The schedule below combines the invited and contributed presentations for the two workshops. We will organize a common, informal dinner for interested participants at the conclusion of the workshops. Note that only the lunch and coffee breaks are covered by the workshops/conference 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

Dinner