<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <div class="moz-text-html" lang="x-unicode">
      <div dir="ltr">
        <p><span style="font-family: Courier\ New, Courier, monospace;">=======================================================================<br>
                                       Call for papers</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">    
            Logical Frameworks and Meta-Languages: Theory and Practice<br>
                                        LFMTP 2018</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">                       
            Oxford, UK, 7 July 2018<br>
                             Affiliated with FSCD 2018 (part of FLoC)</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">                    
            <a href="http://lfmtp.org/workshops/2018/">http://lfmtp.org/workshops/2018/</a></span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">=======================================================================<br>
                          Abstract submission deadline:  8 April 2018<br>
                             Paper submission deadline: 15 April 2018</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">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.</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">LFMTP
            2018 will provide researchers a forum to present
            state-of-the-art<br>
            techniques and discuss progress in areas such as the
            following:</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">*
            Encoding and reasoning about the meta-theory of programming
            languages,<br>
              logical systems and related formally specified systems.</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">*
            Theoretical and practical issues concerning the treatment of
            variable<br>
              binding, especially the representation of, and reasoning
            about,<br>
              datatypes defined from binding signatures.</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">*
            Logical treatments of inductive and co-inductive definitions
            and<br>
              associated reasoning techniques, including inductive types
            of higher<br>
              dimension in homotopy type theory</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">*
            Graphical languages for building proofs, applications in
            geometry,<br>
              equational reasoning and category theory.</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">*
            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.</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">*
            Applications of logical frameworks: proof-carrying
            architectures, proof<br>
              exchange and transformation, program refactoring, etc.</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">*
            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.</span></p>
        <p><br>
          <span style="font-family: Courier\ New, Courier, monospace;">Invited
            Speakers</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">*
            Delia Kesner (Université Paris Diderot, France)<br>
            * Kuen-Bang Hou, alias Favonia (Institute for Advanced
            Study, Princeton, USA)<br>
            * Grigore Rosu (University of Illinois at Urbana-Champaign,
            USA)</span></p>
        <p><br>
          <span style="font-family: Courier\ New, Courier, monospace;">Important
            Dates</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">Abstract
            submission deadline: Sunday   April  8th<br>
            Submission deadline:          Sunday   April 15th<br>
            Notification to authors:      Tuesday  May   15th<br>
            Final version due:            Friday   May   25th<br>
            Workshop date:                Saturday July   7th</span></p>
        <p><br>
          <span style="font-family: Courier\ New, Courier, monospace;">Submission</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">In
            addition to regular papers, we accept the submission of
            "work in progress"<br>
            reports, in a broad sense.  Those do not need to report
            fully polished<br>
            research results, but should be of interest for the
            community at large.<br>
            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=lfmtp18">https://easychair.org/conferences/?conf=lfmtp18</a>.</span></p>
        <p><br>
          <span style="font-family: Courier\ New, Courier, monospace;">Proceedings</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">Accepted
            regular papers will be included in the proceedings of LMFTP<br>
            2018, whose mode of publication will be determined shortly.</span></p>
        <p><br>
          <span style="font-family: Courier\ New, Courier, monospace;">Program
            Committee</span></p>
        <p><span style="font-family: Courier\ New, Courier, monospace;">*
            María Alpuente (Universitat Politècnica de València, Spain)<br>
            * Andrej Bauer (University of Ljubljana, Slovenia)<br>
            * Frédéric Blanqui (Inria, France), co-chair<br>
            * Ana Bove (Chalmers University of Technology, Sweden)<br>
            * Stéphane Graham-Lengrand (CNRS, France)<br>
            * Makoto Hamana (Gunma University, Japan)<br>
            * Chantal Keller (Université Paris-Sud, France)<br>
            * Carlos Olarte (Universidade Federal do Rio grande do
            Norte, Brazil)<br>
            * Giselle Reis (CMU Qatar), co-chair<br>
            * Aaron Stump (University of Iowa, USA)<br>
            * Yuting Wang (Yale University, USA)</span></p>
      </div>
    </div>
  </body>
</html>