|
Session 1 : Welcome, Invited Talk, System Description |
|
Session Chair: Carsten Schürmann |
| 9:00 | - | 10:00 |
Randy Pollack (University of Edinburgh) |
| | | |
Invited Talk |
| |
| 10:00 | - | 10:30 |
Alberto Momigliano, Alan J. Martin and Amy P. Felty. |
| | | |
Two-Level Hybrid: A System for Reasoning Using Higher-Order
Abstract Syntax |
| | | |
System Description |
|
| 10:30 | - | 11:00 |
Break |
|
Session 2: Technology |
|
Session Chair: to be announced |
| 11:00 | - | 11:30 |
William Lovas and Frank Pfenning. |
| | | |
A Bidirectional Refinement Type System for LF
|
| |
| 11:30 | - | 12:00 |
Paul Callaghan. |
| | | |
Coercive subtyping via mappings of reduction behaviour
|
| |
| 12:00 | - | 12:30 |
Brigitte Pientka, Florent Pompigne and Xi Li. |
| | | |
Focusing the inverse method for LF: a preliminary report
|
| |
|
| 12:30 | - | 14:00 |
Lunch |
|
Session 3: Applications |
|
Session Chair: to be announced |
| 14:00 | - | 14:30 |
Julien Narboux and Christian Urban. |
| | | |
Formalisation of the Logical Relation Proof given by Crary for
Completeness of Equivalence Checking |
| |
| 14:30 | - | 15:00 |
Alexandre Buisse and Peter Dybjer. |
| | | |
Formalizing Categorical Models of Type Theory in Type Theory |
| |
| 15:00 | - | 15:30 |
Michael Zeller, Aaron Stump and Morgan Deters. |
| | | |
A Signature Compiler for the Edinburgh LF |
|
| 15:30 | - | 16:00 |
Break |
|
Session 4: Meta-Theory |
|
Session Chair: Brigitte Pientka |
| 16:00 | - | 16:30 |
Anders Schack-Nielsen. |
| | | |
Towards a meta-logic for CLF
|
| |
| 16:30 | - | 17:00 |
Fredrik Lindblad. |
| | | |
Higher-Order Proof Construction Based on First-Order Narrowing.
|
| |
| 17:00 | - | 17:30 |
Murdoch Gabbay and Stephane Lengrand.. |
| | | |
The lambda context calculus.
|
| |