<div dir="ltr">[Apologies if you receive multiple copies of this CFP. Please forward to interested parties]<br><div><br></div><div>===============================================================<br>                **DEADLINE EXTENSION**<br><br>   **New abstract submission deadline: April 20, 2023**<br><br>                          LFMTP 2023<br><br>           Logical Frameworks and Meta-Languages:<br>                   Theory and Practice<br><br>             Rome, Italy -- July 2nd, 2023<br>               Affiliated with FSCD 2023<br><br>              <a href="https://urldefense.com/v3/__https://lfmtp.org/workshops/2023__;!!IBzWLUs!X2UBQiK-V9nj7rsgZ_tW_OxybkoKr5lBHH1fxNWSBl58xOkHvB5Cd8aJxTTC2ygyx49iMmNeaQ1MK4w7eqiXaHhkj0VvGgHf-Et8nA$">https://lfmtp.org/workshops/2023</a> <br><br>===============================================================<br><br>Logical frameworks and meta-languages form a common substrate for<br>representing, implementing and reasoning about a wide variety of<br>deductive systems of interest in logic and computer science. Their<br>design, implementation and their use in reasoning tasks, ranging from<br>the correctness of software to the properties of formal systems,<br>have been the focus of considerable research over the last two decades.<br>This workshop will bring together designers, implementors and<br>practitioners to discuss various aspects impinging on the structure and<br>utility of logical frameworks, including the treatment of variable<br>binding, inductive and co-inductive reasoning techniques and the<br>expressiveness and lucidity of the reasoning process.<br><br>LFMTP 2023 will provide researchers a forum to present state-of-the-art<br>techniques and discuss progress in areas such as the following:<br><br>* Encoding and reasoning about the meta-theory of programming languages,<br>  logical systems and related formally specified systems.<br><br>* Theoretical and practical issues concerning the treatment of variable<br>  binding, especially the representation of, and reasoning about,<br>  datatypes defined from binding signatures.<br><br>* Logical treatments of inductive and co-inductive definitions and<br>  associated reasoning techniques, including inductive types of higher<br>  dimension in homotopy type theory.<br><br>* Graphical languages for building proofs, applications in geometry,<br>  equational reasoning and category theory.<br><br>* New theory contributions: canonical and substructural frameworks,<br>  contextual frameworks, proof-theoretic foundations supporting<br>  binders, functional programming over logical frameworks,<br>  homotopy and cubical type theory.<br><br>* Applications of logical frameworks: proof-carrying architectures,<br>  proof exchange and transformation, program refactoring, etc.<br><br>* Techniques for programming with binders in functional programming<br>  languages such as Haskell, OCaml or Agda, and logic programming<br>  languages such as lambda Prolog or Alpha-Prolog.<br><br>The workshop's program will include contributed and invited talks.<br>We hope that LFMTP takes place physically in Rome, but online<br>participation will be possible and may even be necessary.<br><br>## Important Dates<br><br>Abstract submission deadline: *Extended* April 20 (AoE)<br>Paper submission deadline: *Extended* April 27 (AoE)<br>Notification to authors: May 26<br><br>## Submission<br><br>Submit on EasyChair: <a href="https://urldefense.com/v3/__https://easychair.org/conferences/?conf=lfmtp23__;!!IBzWLUs!X2UBQiK-V9nj7rsgZ_tW_OxybkoKr5lBHH1fxNWSBl58xOkHvB5Cd8aJxTTC2ygyx49iMmNeaQ1MK4w7eqiXaHhkj0VvGgHSdx6drw$">https://easychair.org/conferences/?conf=lfmtp23</a><br><br>All papers must be original and not simultaneously submitted to another <br>journal or conference.<br><br>In addition to regular papers, we welcome/encourage the submission of<br>"work in progress" reports, in a broad sense. Those do not need to<br>report fully polished research results, but should be of interest for<br>the community at large.<br><br>Submitted papers should be in PDF, formatted using the EPTCS style<br>guidelines (<a href="https://urldefense.com/v3/__https://info.eptcs.org/__;!!IBzWLUs!X2UBQiK-V9nj7rsgZ_tW_OxybkoKr5lBHH1fxNWSBl58xOkHvB5Cd8aJxTTC2ygyx49iMmNeaQ1MK4w7eqiXaHhkj0VvGgEbXyLrpQ$">https://info.eptcs.org/</a>). The length is restricted to 15 <br>pages for regular papers and 8 pages for "work in progress" papers<br>(both limits include references).<br><br>## Proceedings<br><br>A selection of the presented papers will be published online in the<br>Electronic Proceedings in Theoretical Computer Science (EPTCS).<br><br>## Invited Speakers<br><br>- Niki Vazou (IMDEA Software Institute Madrid, Spain)<br><br>Note: shared session with LSFA'23 (<a href="https://urldefense.com/v3/__https://sites.google.com/ufg.br/lsfa2023__;!!IBzWLUs!X2UBQiK-V9nj7rsgZ_tW_OxybkoKr5lBHH1fxNWSBl58xOkHvB5Cd8aJxTTC2ygyx49iMmNeaQ1MK4w7eqiXaHhkj0VvGgEaYqw2_Q$">https://sites.google.com/ufg.br/lsfa2023</a>).<br><br>## Program Committee<br><br>* Roberto Blanco (MPI-SP)<br>* Frédéric Blanqui (Inria)<br>* Ana Bove (Chalmers University of Technology)<br>* Alberto Ciaffaglione, co-chair (Università degli Studi di Udine)<br>* Amy Felty (University of Ottawa)<br>* Assia     Mahboubi (Inria) <br>* Narciso Marti-Oliet (Universidad Complutense de Madrid)<br>* Gopalan Nadathur (University of Minnesota)<br>* Carlos Olarte, co-chair (LIPN, Université Sorbonne Paris Nord)<br>* Clément Pit-Claudel (Amazon AWS)<br>* Andrei Popescu (University of Sheffield)<br>* Claudio Sacerdoti Coen (University of Bologna)<br></div></div>