Workshop program:

This year's workshop will feature invited talks, accepted regular papers and work in progress.

8:50am

Welcome!

9:00am

Invited talk:
Dale Miller: Foundational Proof Certificates: Making proof universal and permanent

10:00am

Mahfuza Farooque, St├ęphane Graham-Lengrand and Assia Mahboubi. A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus

10:30am

Break

11:00am

Invited talk:
Furio Honsell: 25 Years of Formal Proof Cultures - some problems, some philosophy, bright future

12:00am

Yuting Wang and Gopalan Nadathur. Towards Extracting Explicit Proofs from Totality Checking in Twelf

12:30am

Lunch

2:00pm

Invited talk:
Bob Harper: CANCELLED

2:30pm

Ulrik Terp Rasmussen and Andrzej Olaf Filinski. Structural Logical Relations with Case Analysis and Equality Reasoning

3:00pm

Andrew Cave and Brigitte Pientka. First-class substitutions in contextual type theory

3:30pm

Break

4:00pm

Floris van Doorn, Herman Geuvers and Freek Wiedijk.Explicit Convertibility Proofs in Pure Type Systems

4:30pm

Vivek Nigam and Elaine Pimentel. Relating Focused Proofs with Different Polarity Assignments

5:00pm

Closing remarks

Accepted Regular Papers (in alphabetical order):

Accepted Work in Progress Report:

Questions: Send email to Brigitte Pientka (bpientka at cs.mcgill.ca)