LFMTP 2021 Program

LFMTP 2021 PROGRAM

Friday, July 16th

Chair:

08:00

Facilitating Meta-Theory Reasoning

Chair:

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

10:00-10:30Break

Chair:

10:30	Johannes Schoisswohl and Laura Kovacs Automating Induction by Reflection (abstract) PRESENTER: Johannes Schoisswohl
11:00	Gilles Dowek Interacting safely with an unsafe environment (abstract)
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 (abstract) PRESENTER: David Baelde

12:00-12:30Break

Chair:

12:30

The MetaCoq Project

Chair:

13:30

Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style (abstract)

PRESENTER: Navid Roux

14:00-14:30Break

Chair:

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