=====================================================

   ACM SIGPLAN International Workshop on Logical Frameworks
    and Meta-Languages: Theory and Practice (LFMTP'13)

           http://complogic.cs.mcgill.ca/lfmtp13

                23 September, 2013 Boston, USA

              Co-located with with ICFP'13

                       CALL FOR PAPERS
 =====================================================

IMPORTANT DATES

Paper submission:        June 14, 2013
Author notification:        July 7, 2013
Final versions due:       July 18, 2013

=====================================================

Logical frameworks and meta-languages form a common substrate for
representing, implementing, and reasoning about a wide variety of
deductive systems of interest in logic and computer science. Their
design and implementation on the one hand and their use in reasoning
tasks ranging from the correctness of software to the properties of
formal computational systems on the other hand have been the focus of
considerable research over the last two decades. This workshop will
bring together designers, implementors, and practitioners to discuss
various aspects impinging on the structure and utility of logical
framework. The broad subject areas of LFMTP'13 are:


* Encoding and reasoning about the meta-theory of programming
languages and related formally specified systems.
* Theoretical and practical issues concerning the treatment of variable
binding.
* Logical treatments of inductive and co-inductive definitions and
associated reasoning techniques.
* New theory contributions: canonical frameworks, contextual
frameworks, functional programming over logical frameworks.

This year's invited speaker are Dale Miller (Inria) and Robert Harper (CMU)
.
In addition, this year LFMTP will celebrate the twenty years anniversary of
the
 publication of:

Robert Harper, Furio Honsell and Gordon Plotkin. A Framework For
Defining Logics. Journal of the Association for Computing Machinery,
40(1):143-184, 1993


Program Committee:
=================

* David Baelde, ENS
* James Cheney, Edinburgh
* Adam Chlipala, MIT
* Dan Licata, CMU/IAS
* Alberto Momigliano, Milano (organizer)
* Brigitte Pientka, McGill (organizer)
* Nicolas Pouillard ITU
* Randy Pollack, Harvard (organizer)
* Andrei Popescu, TUM
* Florian Rabe, Bremen
* Stephanie Weirich, UPenn


Submission Details:
============

In addition to regular papers, we also solicit "work in progress"
report, in a broad sense. Those do not need to report original or
fully polished research results, but should be interesting for the
community at large.

Submitted papers should be in PDF, formatted using the ACM SIGPLAN
style guidelines (9pt format, more details appear on the symposium web
page). The length is restricted to 12 pages, except for "Work in
Progress" papers, which are restricted to 6 pages.

Submission is via EasyChair:

  https://www.easychair.org/conferences/?conf=lfmtp2013

Proceedings:
============

Accepted (regular) papers will be included in the ACM Digital Library.
Authors are encouraged to publish auxiliary material with their paper
(technical appendixes, source code, scripts, test data, etc.).


Travel Support:
===============

Student attendees with accepted papers can apply for a SIGPLAN PAC grant
to help cover travel expenses. PAC also offers other support, such as
for child-care expenses during the meeting or for travel costs for
companions of SIGPLAN members with physical disabilities, as well as for
travel from locations outside of North America and Europe. For details
on the PAC program, see its web page (http://www.sigplan.org/PAC.htm).