Preface

This volume contains a selection of papers presented at LFMTP 2020, the 15th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held the 29-30th of June, 2019, using the Zoom video conferencing tool due to COVID restrictions. Officially the workshop was held in Paris, France, and it was affiliated with IJCAR 2020, FSCD 2020 and many other satellite events.

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 to the workshop, each of which was reviewed by 3 program committee members. Out of those, 8 were selected for presentation. After the workshop we re-opened the submissions for the post-proceedings. We received 6 papers in total, which were either extended versions of the conference papers, or new submissions. Each submission was reviewed again by 3 program committee members. Out of those, 4 were accepted for inclusion in these proceedings.

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 organizers of FSCD-IJCAR 2020 for providing the infrastructure and coordination with other events.

• David Baelde, LSV, ENS Paris-Saclay & Inria Paris
• Frédéric Blanqui, INRIA
• Alberto Ciaffaglione, University of Udine
• Dennis Müller, Friedrich-Alexander-University Erlangen-Nürnberg
• Michael Norrish, Data61
• Carlos Olarte, Universidade Federal do Rio Grande do Norde
• Claudio Sacerdoti Coen, University of Bologna (PC Co-Chair)
• Ulrich Schöpp, fortiss GmbH
• Alwen Tiu, Australian National University (PC Co-Chair)
• Tjark Weber, Uppsala University

A Fresh View of Linear Logic As A Logical Framework

One of the most fundamental properties of a proof system is analyticity, expressing the fact that a proof of a given formula F only uses subformulas of F. In sequent calculus, this property is usually proved by showing that the cut rule is admissible, i.e., the introduction of the auxiliary lemma A in the reasoning "if A follows from B and C follows from A, then C follows from B'' can be eliminated. Mathematically, this means that we can inline the intermediate step A to have a direct proof of B from the hypothesis C. More importantly, the proof of cut-elimination shows that the proof of B follows directly from the axiomatic theory and C (and no external lemmas are needed). The proof of cut-elimination is usually a tedious process through several proof transformations, thus requiring the assistance of (semi-)automatic procedures to avoid mistakes. In a previous work by Miller and Pimentel, linear logic (LL) was used as a logical framework for establishing sufficient conditions for cut-elimination of object logics (OL). The OL's inference rules were encoded as an LL theory and an easy-to-verify criterion sufficed to establish the cut-elimination theorem for the OL at hand. Using such procedure, analyticity of logical systems such as LK (classical logic), LJ (intuitionistic logic) and substructural logics such as MALL (multiplicative additive LL) was proved within the framework. However, there are many logical systems that cannot be adequately encoded in LL, the most symptomatic cases being sequent systems for modal logics. In this talk we will show how to use a linear-nested sequent (LNS) presentation of SLL (a variant of linear logic with subexponentials) and show that it is possible to establish a cut-elimination criterion for a larger class of logical systems, including LNS proof systems for modal logics K, K4, KT, KD, S4 and the multi-conclusion LNS system for intuitionistic logic (mLJ). Impressively enough, the sufficient conditions for cut-elimination presented here remain as simple as the one proposed by Miller and Pimentel. The key ingredient in our developments is the use of the right formalism: we adopt LNS based OL systems, instead of sequent ones. This not only provides a neat encoding procedure of OLs into SLL, but it also allows for the use of the meta-theory of SLL to establish fundamental meta-properties of the encoded OLs. We thus contribute with procedures for checking cut-elimination of several logical systems that are widely used in philosophy, mathematics and computer science.

This is a joint work with Carlos Olarte and Bruno Xavier (UFRN).

Supernominal Datatypes and Codatatypes

Supernominal (co)datatypes form the basis of an expressive mechanism for specifying and reasoning about syntax with bindings. They are a generalization of the nominal logic datatypes having two distinguishing features. First, they go beyond finite support, catering for structures with infinite branching and/or infinite depth. Second, they are compositional: Complex binding structures, such as those proposed in the POPLmark challenge, arise naturally by composing and iterating simpler patterns. Dedicated support for binding-aware (co)recursion and (co)induction also follows from these constructions. A prototype of supernominal (co)datatypes has been formalized in Isabelle/HOL as an extension of the standard (co)datatypes and their underlying Bounded Natural Functors (BNFs). An implementation as a definitional package is under way.

This is a joint work with Jasmin Blanchette, Lorenzo Gheri and Dmitriy Traytel.

The recorded presentation can be found at: https://www.andreipopescu.uk/videos/LFMTP2020_Andrei_Popescu.mp4