[TYPES/announce] LFMTP 2009: Deadline extension
Amy Felty
afelty at site.uottawa.ca
Mon May 4 12:46:46 EDT 2009
***** NOTE: Extended Deadline *****
Final 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 7 (* new date *)
Paper Submission: May 12 (* new date *)
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)
More information about the Types-announce
mailing list