Chair: TBA

• 09:30: Roberto Blanco, Matteo Manighetti, Dale Miller. Linking a lambda Prolog proof checker to the Coq kernel: An extended abstract.
• 10:00: Gabriel Hondet. Expressing Predicate Sub-Typing in Lambda Pi Modulo Theory.
• 10:30: Arve Gengelbach, Tjark Weber. Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading.