Workshop Program

Venue: Online via Zoom.

29 June 2020 (all times are in CEST timezone - UTC+2)

9:15-9:30 Opening: welcome message by the Chairs & a brief overview of house rules
9:30-10:00 Session 1: Formalising logics (chair: Dennis Müller)
09:30
Caitlin D'Abrera and Rajeev Gore
Verified Synthesis of (Very Simple) Sahlqvist Correspondents via Coq extended abstract
10:00
Petros Papapanagiotou and Jacques Fleuriot
Object-level reasoning with logics encoded in HOL Light extended abstract
10:30
Navid Roux and Florian Rabe
Diagram Operators in a Logical Framework extended abstract
11:00-11:30 FSCD/IJCAR virtual coffee break
11:30-14:00 Break
14:00-15:30 Session 2: Proof theory (chair: Alwen Tiu)
14:00
Elaine Pimentel
A fresh view of linear logic as a logical framework slides
15:00
Roberto Blanco, Dale Miller and Alberto Momigliano
On the Proof Theory of Property-Based Testing of Coinductive Specifications, or: PBT to Infinity and beyond extended abstract

30 June 2020 (all times are in CEST timezone - UTC+2)

09:30-11:00 Session 3: Proof assistants and proof certificates (chair: Enrico Tassi)
09:30
Roberto Blanco, Matteo Manighetti and Dale Miller
Linking a lambda Prolog proof checker to the Coq kernel: An extended abstract extended abstract
10:00
Gabriel Hondet
Expressing Predicate Sub-Typing in Lambda Pi Modulo Theory extended abstract
10:30
Arve Gengelbach and Tjark Weber
Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading extended abstract
11:00-11:30 FSCD/IJCAR virtual coffee break
11:30-14:00 Break
14:00-15:30 Session 4: Nominal datatypes and mechanizing metatheory (chair: Claudio Sacerdoti Coen)
14:00
Andrei Popescu
Supernominal Datatypes and Codatatypes slides
15:00
Jacob Errington, Junyoung Jang and Brigitte Pientka
Mechanizing Metatheory Interactively paper