Workshop Program

Institute of Computer Science
Freie Universität Berlin
Room T9.005

08:55-09:00 Welcome
09:00-10:30 Modalities (chair: I. Cervesato)
09:00
Frank Pfenning
Decomposing Modalities
10:00
Furio Honsell, Luigi Liquori, Petar Maksimovic and Ivan Scagnetto
Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks
10:30-11:00
11:00-12:30 Substructural Frameworks (chair: Gopalan Nadathur)
11:00
Vivek Nigam
A Linear Logic Framework with Subexponentials
12:00
Amy Felty, Alberto Momigliano and Brigitte Pientka
An Open Challenge Problem Repository for Systems Supporting Binders
12:30-14:00
14:00-15:30 Logical Relations (chair: Carsten Schürmann)
14:00
Marc Lasson
A Coq plugin for computing logical relations of parametricity
15:00
Andrew Cave and Brigitte Pientka
A Case Study on Logical Relations using Contextual Types
15:30-16:00
16:00-17:30 Rewriting (chair: Amy Felty)
16:00
Roly Perera and James Cheney
Proof-relevant pi calculus
16:30
Cyprien Mangin and Matthieu Sozeau
Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study
17:00
Ronan Saillard
Rewriting Modulo β in the λΠ-calculus Modulo
17:30-18:00 Work in Progress (chair: Kaustuv Chaudhuri)
17:30
Nicolas Guenot and Daniel Gustafsson
Sequent Calculus and Equational Programming
18:00-18:05 Goodbye