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