<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div dir="ltr">
<div dir="ltr">
<div style="color:rgb(0,0,0)">[Apologies if you received multiple copies of this CFP]</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">CALL FOR PAPERS</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">Logical Frameworks and Meta-Languages: Theory and Practice (Post-Proceedings)</div>
<div style="color:rgb(0,0,0)">LFMTP 2020 <a href="https://lfmtp.org/workshops/2020/">
https://lfmtp.org/workshops/2020/</a></div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">Abstract submission deadline: 2 October 2020 </div>
<div style="color:rgb(0,0,0)">Paper submission deadline: 9 October 2020</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">ABOUT LFMTP</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">Logical frameworks and meta-languages form a common substrate for representing,</div>
<div style="color:rgb(0,0,0)">implementing and reasoning about a wide variety of deductive systems of interest</div>
<div style="color:rgb(0,0,0)">in logic and computer science. Their design, implementation and their use in</div>
<div style="color:rgb(0,0,0)">reasoning tasks, ranging from the correctness of software to the properties of</div>
<div style="color:rgb(0,0,0)">formal systems, have been the focus of considerable research over the last two</div>
<div style="color:rgb(0,0,0)">decades. This workshop will bring together designers, implementors and</div>
<div style="color:rgb(0,0,0)">practitioners to discuss various aspects impinging on the structure and utility</div>
<div style="color:rgb(0,0,0)">of logical frameworks, including the treatment of variable binding, inductive</div>
<div style="color:rgb(0,0,0)">and co-inductive reasoning techniques and the expressiveness and lucidity of the</div>
<div style="color:rgb(0,0,0)">reasoning process.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">The LFMTP 2020 workshop adopts a post-proceedings publication model. The</div>
<div style="color:rgb(0,0,0)">workshop itself took place on 29-30 June 2020 online, jointly with IJCAR and</div>
<div style="color:rgb(0,0,0)">FSCD. Now that the workshop has concluded, we solicit submissions of full papers</div>
<div style="color:rgb(0,0,0)">for the post-proceedings of LFMTP 2020, which will go through the normal</div>
<div style="color:rgb(0,0,0)">peer-review process. Submission is open to all; attendance at the workshop is</div>
<div style="color:rgb(0,0,0)">not prerequisite. </div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">Submissions related to the following topics are welcome: * Encoding and</div>
<div style="color:rgb(0,0,0)">reasoning about the meta-theory of programming languages, process calculi and</div>
<div style="color:rgb(0,0,0)">related formally specified systems.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">* Formalisation of model-theoretic and proof-theoretic semantics of logics.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">* Theoretical and practical issues concerning the treatment of variable binding,</div>
<div style="color:rgb(0,0,0)">especially the representation of, and reasoning about, datatypes defined from</div>
<div style="color:rgb(0,0,0)">binding signatures.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">* Logical treatments of inductive and co-inductive definitions and associated</div>
<div style="color:rgb(0,0,0)">reasoning techniques, including inductive types of higher dimension in homotopy</div>
<div style="color:rgb(0,0,0)">type theory.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">* Graphical languages for building proofs and their applications in geometry,</div>
<div style="color:rgb(0,0,0)">equational reasoning and category theory.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">* New theory contributions: canonical and substructural frameworks, contextual</div>
<div style="color:rgb(0,0,0)">frameworks, proof-theoretic foundations supporting binders, functional</div>
<div style="color:rgb(0,0,0)">programming over logical frameworks, homotopy and cubical type theory.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">* Applications of logical frameworks: proof-carrying architectures, proof</div>
<div style="color:rgb(0,0,0)">exchange and transformation, program refactoring, etc.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">* Techniques for programming with binders in functional programming languages</div>
<div style="color:rgb(0,0,0)">such as Haskell, OCaml or Agda, and logic programming languages such as lambda</div>
<div style="color:rgb(0,0,0)">Prolog or Alpha-Prolog.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">* Design and implementation of systems and tools related to meta-languages and</div>
<div style="color:rgb(0,0,0)">logical frameworks</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">IMPORTANT DATES</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">All deadlines are established as the end of day (23:59) AoE.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">* Abstract submission deadline: 2 October 2020 </div>
<div style="color:rgb(0,0,0)">* Paper submission deadline: 9 October 2020 </div>
<div style="color:rgb(0,0,0)">* Notification to authors: 20 November 2020 </div>
<div style="color:rgb(0,0,0)">* Final version due: 4 December 2020 </div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">SUBMISSION INFORMATION</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">Submitted papers should be in PDF, formatted using the EPTCS LaTeX style. The</div>
<div style="color:rgb(0,0,0)">length is restricted to 15 pages.</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">Submission is via EasyChair: <a href="https://easychair.org/my/conference?conf=lfmtp2020">
https://easychair.org/my/conference?conf=lfmtp2020</a> </div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">All submissions will be peer-reviewed and accepted papers will be published in</div>
<div style="color:rgb(0,0,0)">the Electronic Proceedings in Theoretical Computer Science (EPTCS) series. </div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">PROGRAM COMMITTEE</div>
<div style="color:rgb(0,0,0)"><br>
</div>
<div style="color:rgb(0,0,0)">David Baelde, LSV, ENS Paris-Saclay & Inria Paris </div>
<div style="color:rgb(0,0,0)">Frédéric Blanqui, INRIA</div>
<div style="color:rgb(0,0,0)">Alberto Ciaffaglione, University of Udine </div>
<div style="color:rgb(0,0,0)">Dennis Müller, Friedrich-Alexander-University Erlangen-Nürnberg </div>
<div style="color:rgb(0,0,0)">Michael Norrish, Data61 </div>
<div style="color:rgb(0,0,0)">Carlos Olarte, Universidade Federal do Rio Grande do Norde </div>
<div style="color:rgb(0,0,0)">Claudio Sacerdoti Coen, University of Bologna (PC Co-Chair) </div>
<div style="color:rgb(0,0,0)">Ulrich Schöpp, fortiss GmbH </div>
<div style="color:rgb(0,0,0)">Alwen Tiu, Australian National University (PC Co-Chair) </div>
<div style="color:rgb(0,0,0)">Tjark Weber, Uppsala University</div>
</div>
</div>
<p></p>
-- <br>
You received this message because you are subscribed to the Google Groups "Abella" group.<br>
To unsubscribe from this group and stop receiving emails from it, send an email to
<a href="mailto:abella-theorem-prover+unsubscribe@googlegroups.com">abella-theorem-prover+unsubscribe@googlegroups.com</a>.<br>
To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/abella-theorem-prover/CA%2BovoGab90ML0kuEK9pfq_a-Pp%3DugP1m%3DC76mjooeMUVKXQmAA%40mail.gmail.com?utm_medium=email&utm_source=footer">
https://groups.google.com/d/msgid/abella-theorem-prover/CA%2BovoGab90ML0kuEK9pfq_a-Pp%3DugP1m%3DC76mjooeMUVKXQmAA%40mail.gmail.com</a>.<br>
</body>
</html>