[TYPES/announce] Call for Participation: LFMTP'12

[Adam Chlipala]

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

Seventh International Workshop on Logical Frameworks
       and Meta-Languages: Theory and Practice
                    (LFMTP'12)

      http://people.csail.mit.edu/adamc/lfmtp12/

Copenhagen, Denmark, September 9, 2012
Affiliated with the
  International Conference on Functional Programming
      (ICFP'12)

   CALL FOR PARTICIPATION

-------------------------------------------------------------

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
frameworks, including the treatment of variable binding, inductive and
co-inductive reasoning techniques and the expressivity and lucidity of
the reasoning process.

The broad subject areas of LFMTP'12 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, especially the representation of, and reasoning
   about, datatypes defined from binding signatures.
* Logical treatments of inductive and co-inductive definitions and
   associated reasoning techniques.
* 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 are particularly
   welcome.

-------------------------------------------------------------

INVITED TALKS

Brigitte Pientka, title TBD.
Nicolas Pouillard, From de Bruijn to nowadays: The evolution of 
libraries for binding representation.
Robert J. Simmons, A Walk in the Substructural Park.
Stephanie Weirich, A POPLmark retrospective: Using proof assistants in 
programming language research.

CONTRIBUTED PAPER TALKS

Alberto Momigliano, A supposedly fun thing I may have to do again: A 
HOAS encoding of Howe's method.
Chris Martens and Karl Crary, LF in LF: Mechanizing the Metatheory of LF 
in Twelf.
Furio Honsell, Marina Lenisa, Liquori Luigi, Petar Maksimovic and Ivan 
Scagnetto, LFP – A Logical Framework with External Predicates.
Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann 
and Robert J. Simmons, Trace Matching in a Concurrent Logical Framework.


Other details concerning the workshop can be found on its website at 
http://people.csail.mit.edu/adamc/lfmtp12/.

Program Committee:
Nick Benton (Microsoft Research)
Adam Chlipala (MIT, co-chair)
Nils Anders Danielsson (Chalmers University)
Elsa Gunter (University of Illinois, Urbana-Champaign)
Daniel R. Licata (Carnegie Mellon University)
Dale Miller (INRIA)
Frank Pfenning (Carnegie Mellon University)
Carsten Schürmann (IT University of Copenhagen, co-chair)
Matthieu Sozeau (INRIA)