[TYPES/announce] 2nd 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!SEKZI6sxHWnAjbKUGaRs5L8f6yxjVH10KpjF5OPg4JSKS_6dye5oHweaKsaeGBNNc5LPi9ftrSlNbcvAh7OaCQL0ZfCPNYX0pgyWLA$ 
>
> ====================================================================
>
>        Abstract submission deadline: *April 21*, 2026 (AoE)
>        Paper submission deadline: April 28
>        Submission link:https://urldefense.com/v3/__https://submissions.floc26.org/lfmtp/__;!!IBzWLUs!SEKZI6sxHWnAjbKUGaRs5L8f6yxjVH10KpjF5OPg4JSKS_6dye5oHweaKsaeGBNNc5LPi9ftrSlNbcvAh7OaCQL0ZfCPNYVpfouZig$ 
>
>
> 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!SEKZI6sxHWnAjbKUGaRs5L8f6yxjVH10KpjF5OPg4JSKS_6dye5oHweaKsaeGBNNc5LPi9ftrSlNbcvAh7OaCQL0ZfCPNYWbdLsXYw$ ) 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!SEKZI6sxHWnAjbKUGaRs5L8f6yxjVH10KpjF5OPg4JSKS_6dye5oHweaKsaeGBNNc5LPi9ftrSlNbcvAh7OaCQL0ZfCPNYVpfouZig$  .
>
> ## 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/20260413/dbd9ae7a/attachment.htm>