[TYPES/announce] CfP: LFMTP 2026 - Logical Frameworks and Meta-Languages: Theory and Practice

[Sophie Tourret]

====================================================================

                Call for papers -- LFMTP 2026

            Logical Frameworks and Meta-Languages:
                    Theory and Practice

              Lisbon, Portugal, July 24, 2026
                Affiliated with FSCD 2026

      https://urldefense.com/v3/__https://lfmtp.github.io/lfmtp-page/workshops/2026/__;!!IBzWLUs!VSVzn790OkDnlnpldARmOwkQgp7yTE0WB_yEPykdG8RX9i_fpNSrNF3HYQqgVPmbMjsgHEo-uoZraIqUcJVDYTYqjz9CUBhw4x3nLQ$ 

====================================================================

       Abstract submission deadline: April 21, 2026 (AoE)
       Paper submission deadline: April 28
       Submission link:https://urldefense.com/v3/__https://submissions.floc26.org/lfmtp/__;!!IBzWLUs!VSVzn790OkDnlnpldARmOwkQgp7yTE0WB_yEPykdG8RX9i_fpNSrNF3HYQqgVPmbMjsgHEo-uoZraIqUcJVDYTYqjz9CUBjxaMwRxA$ 


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
andutility of logical frameworks, including the treatment of variable
binding, inductive and co-inductive reasoning techniques and the
expressiveness and lucidity of the reasoning process.  Submission
Guidelines

## Submissions

We welcome three kinds of contributions: *regular papers*, *system
descriptions*, and *"work in progress" reports*, in a broad sense.

System descriptions must be accompanied by an artifact containing the
system described. "Work in progress" reports do not need to describe
fully polished research results, but should be of interest for the
community at large.

Submitted papers should be in PDF, formatted using the EPTCS style
(https://urldefense.com/v3/__https://info.eptcs.org/__;!!IBzWLUs!VSVzn790OkDnlnpldARmOwkQgp7yTE0WB_yEPykdG8RX9i_fpNSrNF3HYQqgVPmbMjsgHEo-uoZraIqUcJVDYTYqjz9CUBir6P9jJA$ ) guidelines. The length is restricted
(excluding references) to 15 pages for regular papers, 10 pages for
system descriptions and 8 pages for "work in progress"
papers. Appendices are allowed but will be excluded from the final
paper, and the pc members are not required to take them into account
for their reviews.

Submission is via the FLoC instance of HotCRP:
https://urldefense.com/v3/__https://submissions.floc26.org/lfmtp/__;!!IBzWLUs!VSVzn790OkDnlnpldARmOwkQgp7yTE0WB_yEPykdG8RX9i_fpNSrNF3HYQqgVPmbMjsgHEo-uoZraIqUcJVDYTYqjz9CUBjxaMwRxA$  .

## List of Topics

LFMTP 2026 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, logical systems and related formally specified
    systems.
  - 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.

## Schedule

  - Abstract submission deadline: April 21
  - Submission deadline: April 28
  - Notifiation to authors : May 28
  - early registration: June 1
  - Final version due: June 10
  - Workshop: July 24 (confirmed)

## Program Committee

Oliver Hermant (Chair, Mines Paris PSL)
Miguel Pagano (Universidad Nacional de Córdoba)
Elaine Pimentel (UCL)
Loïc Pujet (Stockholm University)
Florian	Rabe (FAU Erlangen-Nürnberg)
Alvaro Tasistro (Universidad ORT Uruguay)
Alwen Tiu (The Australian National University)
Sophie Tourret (Chair, INRIA and MPI for Informatics)
Niccolò	Veltri (Tallinn University of Technology)
Yiming	Xu (LMU Munich)

## Invited Speakers

TBA

## Publication

A selection of the presented papers will be published online in the
Electronic Proceedings in Theoretical Computer Science (EPTCS).

## Venue

The conference will be held in Lisbon, Portugal, 24 July 2026. LFMTP
2026 is a workshop affiliated with FLOC 2026.  Contact

All questions about LFMTP 26 should be emailed to lfmtp26_chairs 'at'
inria.fr .

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20260304/b4b368ec/attachment-0001.htm>