# Workshop program:

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

8:50am |
Welcome! |

9:00am |
Invited talk: |

10:00am |
Mahfuza Farooque, Stéphane Graham-Lengrand and Assia Mahboubi. |

10:30am |
Break |

11:00am |
Invited talk: |

12:00am |
Yuting Wang and Gopalan Nadathur. |

12:30am |
Lunch |

2:00pm |
Invited talk: |

2:30pm |
Ulrik Terp Rasmussen and Andrzej Olaf Filinski. |

3:00pm |
Andrew Cave and Brigitte Pientka. |

3:30pm |
Break |

4:00pm |
Floris van Doorn, Herman Geuvers and Freek Wiedijk. |

4:30pm |
Vivek Nigam and Elaine Pimentel. |

5:00pm |
Closing remarks |

## Accepted Regular Papers (in alphabetical order):

- Andrew Cave and Brigitte Pientka.
*First-class substitutions in contextual type theory* - Floris van Doorn, Herman Geuvers and Freek Wiedijk.
*Explicit Convertibility Proofs in Pure Type Systems* - Mahfuza Farooque, Stéphane Graham-Lengrand and Assia Mahboubi.
*A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus* - Ulrik Terp Rasmussen and Andrzej Olaf Filinski.
*Structural Logical Relations with Case Analysis and Equality Reasoning* - Yuting Wang and Gopalan Nadathur.
*Towards Extracting Explicit Proofs from Totality Checking in Twelf*

## Accepted Work in Progress Report:

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

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