<div dir="ltr">=============================================================<br>                           Call for papers<br> Logical Frameworks and Meta-Languages: Theory and Practice<br>                            LFMTP 2021<br><br>                        Pittsburgh, USA, 16 July 2021<br>                         Affiliated with CADE-28<br><br>                     <a href="http://lfmtp.org/workshops/2021/">http://lfmtp.org/workshops/2021/</a><br>=============================================================<br>        Abstract submission deadline: 19 April 2021<br>        Paper submission deadline: 26 April 2021<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<br>systems, have been the focus of considerable research over the last two<br>decades. 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 2021 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, proof<br>  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>Important Dates<br><br>Abstract submission deadline: Monday   April 19<br>Submission deadline:              Monday   April 26<br>Notification to authors:             Monday   May 31<br>Final version due:                    Monday   June 14<br>Workshop date:                       Friday   July  16<br><br>Submission<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 report <br>fully polished research results, but should be of interest for the community <br>at large. Submitted papers should be in PDF, formatted using the EPTCS style<br>guidelines. The length is restricted to 15 pages for regular papers and<br>8 pages for "Work in Progress" papers.  Submission is via EasyChair:<br><a href="https://easychair.org/conferences/?conf=lfmtp2021">https://easychair.org/conferences/?conf=lfmtp2021</a><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>*  Giselle Reis (CMU-Qatar)<br>*  Matthieu Sozeau (Inria) <br><br>Program Committee<br><br>* David Baelde (LSV, ENS Paris-Saclay & Inria Paris)<br>* Roberto Blanco (MPI-SP)<br>* Alberto Ciaffaglione (University of Udine)<br>* Claudio Sacerdoti Coen (University of Bologna)   <br>* Marina Lenisa (Università degli Studi di Udine)<br>* Dennis Müller (Friedrich-Alexander-University)<br>* Michael Norrish (CSIRO)  <br>* Elaine Pimentel (Universidade Federal do Rio Grande do Norte) co-chair  <br>* Ulrich Schöpp (fortiss GmbH)    <br>* Kathrin Stark (Princeton University)<br>* Aaron Stump (The University of Iowa)    <br>* Nora Szasz (Universidad ORT Uruguay)<br>* Enrico Tassi (Inria) co-chair<br>* Alwen Tiu (The Australian National University)   <br>* Tjark Weber (Uppsala University)<br><div><br></div></div>