Workshop Program

09:20-09:30 Welcome Message Marino Miculan and Florian Rabe
09:30-11:00 Session 1 (chair: Marino Miculan)
09:30
Andrew Appel
Verifiable C, a Higher-order Impredicative Concurrent Separation Logic in Coq
10:30
Andreas Abel, Alberto Momigliano and Brigitte Pientka
POPLMark Reloaded
11:00-11:30 Morning tea break
11:30-13:00 Session 2 (chair: Andreas Abel)
11:30
Jeff Polakow
Uniform Atomic Ordered Linear Logic
12:00
Claude Stolze, Luigi Liquori, Furio Honsell and Ivan Scagnetto
Towards a Logical Framework with Intersection and Union Types
12:30
Yuito Murase
Kripke-Style Contextual Modal Type Theory
13:00-14:00 Lunch break
14:00-15:30 Session 3 (chair: Brigitte Pientka)
14:00
Roberto Blanco, Dale Miller and Alberto Momigliano
Property-Based Testing via Proof Reconstruction: Work-in-progress
14:30
Michael D. Ariotti and John Tang Boyland
Making Substitutions Explicit in SASyLF
15:00
Jonas Kaiser, Steven Schäfer and Kathrin Stark
Autosubst 2: Towards Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
15:30-16:00 Afternoon tea break
16:00-17:30 Session 4 (dedicated to Randy Pollack) (chair: Alberto Momigliano)
16:00
Randy Pollack
Beta reduction without rule ξ
16:30
James McKinna
Names, Places, and Things; fragments of a partial intellectual biography of Randy Pollack
19:15-??:?? Workshop Dinner
We meet for a joint dinner at 4500 Miles from Delhi at 19:15. All attendants and friends of LFMTP are welcome to join. The restaurant is about 1 kilometer south of the workshop venue. Some of us will meet at 18:50 at the workshop venue to walk there together.