Workshop Program

Venue: Lecture Theatre 2, Mathematical Institute, Radcliffe Observatory Quarter, Woodstock Road.

The program is also available on the FLOC website.

09:00-10:30

Type Theory and Proof Assistants

(chair: Enrico Tassi)

09:00	Kuen-Bang Hou (Favonia) Cubical Computational Type Theory and RedPRL slides
10:00	François Thiré Sharing a library between proof assistants: reaching out to the HOL family slides

10:30-11:00

11:00-12:30

Verification and Testing

(chair: Giselle Reis)

11:00	Grigore Rosu Why and How Does K work? The Logical Infrastructure Behind It slides
12:00	Kaustuv Chaudhuri, Ulysse Gérard and Dale Miller Computation-as-deduction in Abella: work in progress slides
12:20	Francesco Komauli and Alberto Momigliano Property-Based Testing of Abstract Machines: an Experience Report slides

12:40-14:00

14:00-15:30

Formalization

(chair: Brigitte Pientka)

14:00	Martin Copes, Nora Szasz and Alvaro Tasistro Formalization in Constructive Type Theory of the Standardization Theorem slides
14:30	Ernesto Copello, Nora Szasz and Alvaro Tasistro Formalisation of Barendregt's Variable Convention for Generic Structures with Binders slides
15:00	David Feller, Joe Wells, Sébastien Carlier and Fairouz Kamareddine What Does This Notation Mean Anyway? BNF-style notation as it is actually used slides

15:20-16:00

16:00-17:50

Implementation

(chair: Stéphane Graham-Lengrand)

16:00	Delia Kesner A fresh view of call-by-need slides
17:00	Rodolphe Lepigre and Christophe Raffalli Abstract Representation of Binders in OCaml using the Bindlib Library slides
17:30	Ulysse Gérard and Dale Miller Functional programming with λ-tree syntax: a progress report slides

19:00-21:00

(distinct from FLoC workshop dinner)

If you want to join, send a mail before July 1st.