Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Alberto Momigliano <amomigl1@inf.ed.ac.uk>
International Workshop on Logical Frameworks and Meta-Languages:
Theory and Practice (LFMTP'06)
http://www.cs.mcgill.ca/~bpientka/lfmtp06/index.html
Affiliated with LICS and IJCAR at FLOC'06
Seattle, Washington, 16 August, 2006.
CALL FOR PAPERS
Important Dates:
Submission deadline: 15 May 2006
Author Notification: 15 June 2006
Final Version: 15 July 2006
LFMTP'06 merges the International workshop on Logical Frameworks
and Meta-languages (LFM) and the MERLIN workshop on MEchanized
Reasoning about Languages with variable BIndingIN).
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 one hand and their applications, for
example, to proof-carrying code have been the focus of considerable
research over the last two decades. This workshop will bring together
designers, implementors, and practitioners to discuss all aspects of
logical frameworks.
The broad subject areas of LFMTP'06 are:
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 theoretical and practical issues concerning the encoding of
variable binding and fresh name generation, 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 programming languages and calculi. Papers focusing on
experiences with encoding programming languages theory and instances
of proof-carrying code or proof-carrying authorization are
particularly welcome.
Topics include, but are 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
* sub-structural frameworks
* semantic foundations
* methods for reasoning about logics
* case studies.
Invited Speaker: Gordon Plotkin (University of Edinburgh).
Program Committee:
Andrew Appel Princeton University
Thierry Coquand Goteborg University
Martin Hofmann LMU Munich
Furio Honsell University of Udine
Dale Miller Inria Futurs
Brigitte Pientka McGill University
Andrew Pitts Cambridge University
Kevin Watkins Carnegie Mellon University
Paper Submissions.
Three categories of papers are solicited:
* Category A: Detailed and technical accounts of new research: up
to fifteen pages including bibliography.
* Category B: Shorter accounts of work in progress and proposed
further directions, including discussion papers: up to eight
pages including bibliography.
* Category C: System descriptions, presenting an implemented tool
and its novel features: up to six pages. A demonstration is
expected to accompany the presentation.
Submission is electronic in postscript or PDF format. Submitted papers
must conform to the ENTCS style, preferably using LaTeX2e. For further
information and submission instructions, see the LFMTP web page:
http://www.cs.mcgill.ca/~bpientka/lfmtp06/index.html
Proceedings are to be published as a volume in the Electronic Notes in
Theoretical Computer Science (ENTCS) series and will be available to
participants at the workshop.
Organizers:
Brigitte Pientka Alberto Momigliano
bpientka@cs.mcgill.ca amomigl1@inf.ed.ac.uk
School of Computer Science LFCS, School of Informatics
McGill University University of Edinburgh
Last updated: Nov 21 2024 at 12:39 UTC