[TYPES/announce] LFMTP 2009: Call for Papers

[Amy Felty]

                              Call for Papers
                 LFMTP 2009: 4th International Workshop on
        Logical Frameworks and Meta-languages: Theory and Practice
                    McGill University, Montreal, Canada
                              August 2, 2009
                    http://workshops.inf.ed.ac.uk/lfmtp

Affiliated with CADE-22, Montreal, Canada, August 2-7, 2009
Joint event with the 2009 International Workshop on Proof-Search in
Type Theories (PSTT), August 3, 2009

IMPORTANT DATES
Abstract submission:   May 1
Paper Submission:   May 8
Notification:   June 15
Final papers due:   July 3
Workshop:   August 2

JOINT LFMTP/PSTT INVITED SPEAKER:
  Gilles Dowek (Ecole Polytechnique & INRIA)
JOINT LFMTP/PSTT TUTORIAL SPEAKER:
  TBA

DESCRIPTION: The LFMTP workshop continues a series of workshops on
Logical Frameworks and Metalanguages (LFM) and Mechanized Reasoning
about Languages with Variable Binding (MERLIN).  This is the fourth
joint workshop in the series.

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.  LFMTP
2009 will provide researchers with a forum to review state-of-the-art
techniques and to present progress in:
- the automation and implementation of the meta-theory of programming
  languages and related calculi, particularly work which involves
  variable binding and fresh name generation;
- the design of proof assistants, automated theorem provers, and
  formal digital libraries building upon logical framework technology;
- theoretical and practical issues concerning the encoding of variable
  binding, especially the representation of, and reasoning about,
  datatypes defined from binding signatures;
- case studies of meta-programming, and the mechanization of the
  (meta) theory of descriptions of programming languages and other
  calculi.  Papers focusing on logic translations and on experiences
  with encoding programming languages theory will be particularly
  welcome.

TOPICS: Papers are solicited on topics including, but not limited to:
- logical framework design
- meta-theoretic analysis
- applications and comparative studies
- implementation techniques
- efficient proof representation and validation
- proof-generating decision procedures and theorem provers
- proof-carrying code
- substructural frameworks
- semantic foundations
- methods for reasoning about logics
- formal digital libraries

SUBMISSIONS: Three categories of papers are solicited:
- Category A: Detailed and technical accounts of new research: up to
  eight pages including bibliography.
- Category B: Shorter accounts of work in progress and proposed
  further directions, including discussion papers: up to six pages
  including bibliography and appendices.
- Category C: System descriptions presenting an implemented tool and
  its novel features: up to four pages.  A demonstration is expected
  to accompany the presentation.

Submissions will be accepted electronically. Authors are required to
submit a paper title and a short abstract one week before submitting
the paper.  For further information and submission instructions, see
the LFMTP web page: http://workshops.inf.ed.ac.uk/lfmtp.
Accepted papers will be published electronically as part of the ACM
International Conference Proceedings Series.

Authors of accepted papers are expected to present their paper at the
workshop.

PROGRAM COMMITTEE:
  Frederic Blanqui (INRIA)
  James Cheney, Co-Chair (University of Edinburgh)
  Adam Chlipala (Harvard University)
  Amy Felty, Co-Chair (University of Ottawa)
  Martin Hofmann (LMU Munich)
  Conor McBride (University of Strathclyde)
  Marino Miculan (University of Udine)
  Alberto Momigliano (University of Edinburgh)
  Gopalan Nadathur (University of Minnesota)
  Michael Norrish (NICTA)