CADE-28: THE 28TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION
LFMTP 2021 PROGRAM
Friday, July 16th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:00 Session 36A: LFMTP Workshop: Meta-Theory Reasoning
Location: ZoomRoom 3
09:00
SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts (abstract)
PRESENTER: Laila El-Beheiry
09:30
Countability of Inductive Types Formalized in the Object-Logic Level (abstract)
PRESENTER: Xiwei Wu
10:00-10:30Break
10:30-12:00 Session 37D: LFMTP Workshop: Foundations
Location: ZoomRoom 3
10:30
Automating Induction by Reflection (abstract)
11:00
Interacting safely with an unsafe environment (abstract)
11:30
Foundations of the Squirrel meta-logic for reasoning over security protocols (abstract)
PRESENTER: David Baelde
12:00-12:30Break
13:30-14:00 Session 40: Foundations: MetaCoq
Location: ZoomRoom 3
13:30
Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style (abstract)
PRESENTER: Navid Roux
14:00-14:30Break
14:30-16:00 Session 41C: LFMTP Workshop: Formalization
Location: ZoomRoom 3
14:30
Adelfa: A System for Reasoning about LF Specifications (abstract)
PRESENTER: Mary Southern
15:00
A logical framework with a graph meta-language (abstract)
PRESENTER: Bruno Cuconato
15:30
Towards a Semantic Framework for Policy Exchange in the Internet (abstract)