Last update: 2020-08-26
UPDATES (2020-08-26):
LFMTP 2020 now solicits submissions for the Post-Proceedings.
Abstract deadline: 2 October 2020
Paper deadline: 9 October 2020
For details, see the LFMTP 2020 Post-Proceedings Call for Papers.
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.
LFMTP 2020 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following:
- Encoding and reasoning about the meta-theory of programming languages, process calculi and related formally specified systems.
- Formalisation of model-theoretic and proof-theoretic semantics of logics.
- Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures.
- Logical treatments of inductive and co-inductive definitions and associated reasoning techniques, including inductive types of higher dimension in homotopy type theory.
- Graphical languages for building proofs, applications in geometry, equational reasoning and category theory.
- New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy and cubical type theory.
- Applications of logical frameworks: proof-carrying architectures, proof exchange and transformation, program refactoring, etc.
- Techniques for programming with binders in functional programming languages such as Haskell, OCaml or Agda, and logic programming languages such as lambda Prolog or Alpha-Prolog.
- Design and implementation of systems and tools related to meta-languages and logical frameworks.
Venue
LFMTP 2020 will be held online, as part of the FSCD-IJCAR satelite events. For the details of the arrangment, we refer to the FSCD-IJCAR website.
Program
See the program.
Registration
Please see register via IJCAR-FSCD 2020 Registration page.
Invited Speakers
- Elaine Pimentel, Universidade Federal do Rio Grande do Norte, Brazil.
- Andrei Popescu, University of Sheffield, UK.
For information about titles and abstracts, see Invited Talks.
List of accepted presentations
- Petros Papapanagiotou and Jacques Fleuriot. Object-level reasoning with logics encoded in HOL Light.
- Jacob Errington, Junyoung Jang and Brigitte Pientka. Mechanizing Metatheory Interactively.
- Roberto Blanco, Dale Miller and Alberto Momigliano. On the Proof Theory of Property-Based Testing of Coinductive Specifications, or: PBT to Infinity and beyond.
- Roberto Blanco, Matteo Manighetti and Dale Miller. Linking a lambda Prolog proof checker to the Coq kernel: An extended abstract.
- Gabriel Hondet. Expressing Predicate Sub-Typing in Lambda Pi Modulo Theory.
- Navid Roux and Florian Rabe. Diagram Operators in a Logical Framework.
- Arve Gengelbach and Tjark Weber. Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading.
- Caitlin D'Abrera and Rajeev Gore. Verified Synthesis of (Very Simple) Sahlqvist Correspondents via Coq.
Important Dates
Updates (2020-08-26): Submission for post-proceedings is now open. See the Post-Proceedings section below for details.
Updates (2020-06-14): The workshop schedule has been rescheduled to last for two days: 29 - 30 June 2020.
Updates (2020-04-16): Submission deadlines extended.
All deadlines are established as the end of day (23:59) AoE.
May 18, 202: Submission deadlineJune 1, 2020: Notification to authorsJune 29 - 30, 2020: Workshop
Submission
We solicit submissions of long abstracts describing original research results or descriptions of work in progress. The topics of the submissions should be of interest to the LFMTP community at large. Submitted abstracts should be in PDF, formatted using the EPTCS LaTeX style. The length is restricted to 2 pages. All submissions will undergo a light peer-review process and the authors of those accepted will be invited to present their papers at the workshop.
Submission is via EasyChair.
Post-Proceedings Submissions
Submission for the post-proceedings is now open. Submission is open to all; attendance at the workshop is not a prerequisite. Submitted papers should be in PDF, formatted using the EPTCS LaTeX style. The length is restricted to 15 pages.
Submission is via EasyChair: https://easychair.org/my/conference?conf=lfmtp2020
All submissions will be peer-reviewed and accepted papers will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series.
Important Dates (post-proceedings)
- October 2, 2020: Abstract submission
- October 9, 2020: Paper submission
- November 20, 2020: Notification to authors
- December 4, 2020: Final version due
Program Committee
- 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
Organizer
Claudio Sacerdoti Coen and Alwen Tiu.
Contact: LFMTP 2020 PC Chairs