| SESSION 1: 9:00-10:30 |
|---|
| 9:00-10:00 |
Brigitte Pientka, Belugamu: Programming proofs in context |
| 10:00-10:30 |
Alberto Momigliano, A supposedly fun thing I may have to do again: A HOAS encoding of Howe's method |
|
| BREAK: 10:30-11:00 |
|---|
|
| SESSION 2: 11:00-12:30 |
|---|
| 11:00-12:00 |
Nicolas Pouillard, From de Bruijn to nowadays: The evolution of libraries for binding representation |
| 12:00-12:30 |
Furio Honsell, Marina Lenisa, Liquori Luigi, Petar Maksimovic and Ivan Scagnetto, LFP – A Logical Framework with External Predicates |
|
| LUNCH: 12:30-14:00 |
|---|
|
| SESSION 3: 14:00-15:30 |
|---|
| 14:00-15:00 |
Robert J. Simmons, A Walk in the Substructural Park |
| 15:00-15:30 |
Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann and Robert J. Simmons, Trace Matching in a Concurrent Logical Framework |
|
| BREAK: 15:30-16:00 |
|---|
|
| SESSION 4: 16:00-17:30 |
|---|
| 16:00-16:30 |
Chris Martens and Karl Crary, LF in LF: Mechanizing the Metatheory of LF in Twelf |
| 16:30-17:30 |
Stephanie Weirich, A POPLmark retrospective: Using proof assistants in programming language research |
