# CFP LFMTP26, Logical Frameworks and Meta-Languages: Theory and Practice @FLOC, Lisbon, Portugal, July 24

**URL:** <https://discourse.rocq-prover.org/t/cfp-lfmtp26-logical-frameworks-and-meta-languages-theory-and-practice-floc-lisbon-portugal-july-24/3002>\
**Category:** Announcements\
**Tags:** cfp\
**Created:** [March 26, 2026, 5:30pm UTC](https://discourse.rocq-prover.org/t/cfp-lfmtp26-logical-frameworks-and-meta-languages-theory-and-practice-floc-lisbon-portugal-july-24/3002 "2026-03-26T17:30:43Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![olivhash](https://avatars.discourse-cdn.com/v4/letter/o/a587f6/32.png) [@olivhash](https://discourse.rocq-prover.org/u/olivhash)\
**Post date:** [March 26, 2026, 5:30pm UTC](https://discourse.rocq-prover.org/t/cfp-lfmtp26-logical-frameworks-and-meta-languages-theory-and-practice-floc-lisbon-portugal-july-24/3002/1 "2026-03-26T17:30:43Z")

</div>

```auto
====================================================================

               Call for papers -- LFMTP 2026

           Logical Frameworks and Meta-Languages:
                   Theory and Practice

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

     https://lfmtp.github.io/lfmtp-page/workshops/2026/

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

      Abstract submission deadline: April 21, 2026 (AoE)
      Paper submission deadline: April 28, 2026 (AoE)
      Submission link: https://submissions.floc26.org/lfmtp/

```

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.

## 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://info.eptcs.org/](https://info.eptcs.org/)) 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://submissions.floc26.org/lfmtp/](https://submissions.floc26.org/lfmtp/) .

## 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
- Notification to authors: May 28
- early registration: June 1
- Final version due: June 10
- Workshop: July 24

## 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](http://inria.fr) .