Program of MLPA

Thursday, July 15th

Thursday's program is also available with abstracts and side by side with other events.

09:00‑10:00 Invited talk
Location: IF 1.16
09:00 Ulf Norell (Chalmers University)
Modules and records in Agda
10:30‑12:30 Invited talks
Location: IF 1.16
10:30 Gerwin Klein (University of New South Wales)
Large-scale proof and libraries in Isabelle
11:30 Andrzej Trybulec (University of Bialystok)
Mizar Mathematical Library - a large repository of formalized mathematics
14:00‑15:00 Invited talk
Location: IF 1.16
14:00 Don Sannella (University of Edinburgh)
Proofs in structured specifications
15:30‑17:30 Invited talks
Location: IF 1.16
15:30 Dale Miller (INRIA)
Towards a broad spectrum proof certificate
16:30 Adam Chlipala (Harvard University)
A Bottom-Up Approach to Safe Low-Level Programming