<div dir="ltr"><div><br></div>===============================================================<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!WnWI7wsrVwoehc9aYJUaRT8ZOtWp-s41yE-sGvp5hg6wlj2waxvAd82NMpuRDpZ34rgiPljTuoX9QnUBA00Lk5-0mIj93QlYnmwq6Q$">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>## 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!WnWI7wsrVwoehc9aYJUaRT8ZOtWp-s41yE-sGvp5hg6wlj2waxvAd82NMpuRDpZ34rgiPljTuoX9QnUBA00Lk5-0mIj93QkGCF4Nzw$">https://sites.google.com/ufg.br/lsfa2023</a>).<br><br>## Registration<br><br>Online registration fee available! <br><a href="https://urldefense.com/v3/__https://easyconferences.eu/fscd2023/registration1/__;!!IBzWLUs!WnWI7wsrVwoehc9aYJUaRT8ZOtWp-s41yE-sGvp5hg6wlj2waxvAd82NMpuRDpZ34rgiPljTuoX9QnUBA00Lk5-0mIj93QkI_p8TUQ$">https://easyconferences.eu/fscd2023/registration1/</a><br></div>