Published: 16th July 2021
DOI: 10.4204/EPTCS.337
ISSN: 2075-2180


Proceedings Sixteenth Workshop on
Logical Frameworks and Meta-Languages: Theory and Practice
Pittsburgh, USA, 16th July 2021

Edited by: Elaine Pimentel and Enrico Tassi

Elaine Pimentel and Enrico Tassi
Facilitating Meta-Theory Reasoning (Invited Paper)
Giselle Reis
Touring the MetaCoq Project (Invited Paper)
Matthieu Sozeau
Interacting Safely with an Unsafe Environment
Gilles Dowek
Automating Induction by Reflection
Johannes Schoisswohl and Laura Kovács
Countability of Inductive Types Formalized in the Object-Logic Level
Qinxiang Cao and Xiwei Wu
SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts
Laila El-Beheiry, Giselle Reis and Ammar Karkour
Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style
Florian Rabe and Navid Roux
Adelfa: A System for Reasoning about LF Specifications
Mary Southern and Gopalan Nadathur


This volume contains a selection of papers presented at LFMTP 21, the 16th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held on July 16, 2021 using the Zoom video conferencing tool due to COVID restrictions. The workshop was affiliated with CADE-28.

Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.

We received 11 submissions in total, which were reviewed by 3 program committee members. Out of those, 3 were selected as work in progress reports for presentation and 6 were selected for presentation and publication. Each submission selected for publication was reviewed again by 3 program committee members and included in these proceedings.

In addition to the submission presentations, the program included 2 invited talks by Giselle Reis (CMU, Qatar) "Facilitating Meta-Theory Reasoning" and Matthieu Sozeau (Inria, France) "The MetaCoq Project".

We want to thank the members of the Program Committee for their efforts in providing timely reviews and for the useful suggestions and participation on the decisions. Moreover, we want to thank the authors and the invited speakers, since their contributions and presentations at the meeting stimulated interesting discussions with the attendees, making the event a success. We are also very grateful to the organization of CADE-28 for providing the infrastructure and coordination with other events.

Program Committee of LFMTP 2021:

We are grateful to the external referees Furio Honsell and Pietro Di Gianantonio for their excellent work in reviewing and selecting the submitted papers.

16th of July, 2021 Elaine Pimentel
Enrico Tassi