|
Published: 16th July 2021 DOI: 10.4204/EPTCS.337 ISSN: 2075-2180 |
| Preface Elaine Pimentel and Enrico Tassi | |
| Facilitating Meta-Theory Reasoning (Invited Paper) Giselle Reis | 1 |
| Touring the MetaCoq Project (Invited Paper) Matthieu Sozeau | 13 |
| Interacting Safely with an Unsafe Environment Gilles Dowek | 30 |
| Automating Induction by Reflection Johannes Schoisswohl and Laura Kovács | 39 |
| Countability of Inductive Types Formalized in the Object-Logic Level Qinxiang Cao and Xiwei Wu | 55 |
| SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts Laila El-Beheiry, Giselle Reis and Ammar Karkour | 71 |
| Systematic Translation of Formalizations of Type Theory from Intrinsic to Extrinsic Style Florian Rabe and Navid Roux | 88 |
| Adelfa: A System for Reasoning about LF Specifications Mary Southern and Gopalan Nadathur | 104 |
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 |