Workshop Program

Venue: Room 2280, SFU Harbour Centre in Downtown Vancouver. Address: 515 W Hastings St, Vancouver, BC V6B 5K3, Canada.

8:00-9:00 (near room 2945)

10:30-12:30

1st session

(chair: Ivan Scagnetto)

10:30	Brigitte Pientka Cocon: A Type Theory for Defining Logics and Proofs slides
11:30	Dennis Müller and Florian Rabe Rapid Prototyping Formal Systems in MMT: 5 Case Studies slides
12:00	François Thiré Cumulative Types Systems and levels slides

12:30-14:00 (near room 2945)

14:00-15:30

2nd session

(chair: Dale Miller)

14:00	Chris Hawblitzel Combining tactics, normalization, and SMT solving to verify systems software slides
15:00	Aaron Stump Towards Higher-Order Abstract Syntax in Cedille (Work in Progress) slides

15:30-16:00 (near room 2945)

16:00-17:00

3rd session

(chair: Ivan Scagnetto)

16:00	Michael Kohlhase and Jan Frederik Schaefer GF + MMT = GLF - From Language to Semantics through LF slides
16:30	Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell and Marina Lenisa A definitional implementation of the Lax Logical Framework LLFP in Coq slides