Workshop Program

The Proceedings of LFMTP 2021 appears as the EPTCS 337 volume.

All times are EDT. The program is also available at the CADE-28 website.

08:00-10:00

Meta-Theory Reasoning

(chair: Elaine Pimentel)

08:00	Giselle Reis Facilitating Meta-Theory Reasoning paper
09:00	Laila El-Beheiry, Giselle Reis and Ammar Karkour SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts paper
09:30	Qinxiang Cao and Xiwei Wu Countability of Inductive Types Formalized in the Object-Logic Level paper

10:00-10:30

10:30-12:00

Foundations

(chair: Florian Rabe)

10:30	Johannes Schoisswohl and Laura Kovacs Automating Induction by Reflection paper
11:00	Gilles Dowek Interacting safely with an unsafe environment paper
11:30	David Baelde, Stephanie Delaune, Charlie Jacomme, Adrien Koutsos and Solène Moreau, Foundations of the Squirrel meta-logic for reasoning over security protocols paper

12:00-12:30

12:30-14:00

MetaCoq

(chair: Enrico Tassi)

12:30	Matthieu Sozeau The MetaCoq Project paper
13:30	Florian Rabe and Navid Roux Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style paper

14:00-14:30

14:30-16:00

Formalization

(chair: Giselle Reis)

14:30	Mary Southern and Gopalan Nadathur Adelfa: A System for Reasoning about LF Specifications paper
15:00	Bruno Cuconato, Jefferson de Barros Santos and Edward Hermann Haeusler A logical framework with a graph meta-language paper
15:30	Anduo Wang Towards a Semantic Framework for Policy Exchange in the Internet