LFM 2000 (Logical Frameworks and Meta-languages) - 1st Call for Papers

Dear all,

  Please find below a call for papers for a workshop on LOGICAL
FRAMEWORKS who might be of interest to the members of the Types
community. (The main connection with type systems beeing that many
logical frameworks developped over the last decade have been based on
various type theories.)

  Best regards,
  Joelle Despeyroux
- ---------

                          CALL FOR PAPERS

                       LICS'2000 Workshop on


          Sunday, June 25, 2000, Santa Barbara, California


Logical frameworks and meta-languages are intended as a common
substrate for representing and implementing a wide variety of logics
and formal systems.  Their definition and implementation have been the
focus of considerable work over the last decade.  At the heart of this
work is a quest for generality: A logical framework provides a basis
for capturing uniformities across deductive systems and support for
implementing particular systems.  Similarly a meta-language supports
reasoning about and using languages.

  This workshop will bring together designers, implementers, and
practitioners to discuss the development of logical frameworks and
their use in meta-reasoning and programming.  Topics include (but are
not limited to): the design of logical frameworks, meta-theoretical
studies, comparative studies, implementation, techniques of
representation of formal systems, proofs of properties of formal
systems, program development and proofs of program correctness.

  The workshop will be held on Sunday, June 25, 2000 at Santa Barbara,
California.  It will be held as part of the International Conference
on Logic in Computer Science (LICS'2000), which takes place from June
26 to June 29, at Santa Barbara, California, United States.  (See

  Submissions on any aspect of logical frameworks and meta-languages are
solicited, including papers on work in progress and more mature work.
The submission deadline is April 25, 2000.  Authors will be notified
of acceptance by May 15, 2000.  The final version of accepted papers
will be due by June 9, 2000.  Submitted papers should be extended
abstracts of 7-10 pages.  Please submit your abstract electronically
by mailing a uuencoded compressed (or gziped) postscript file to
lfm2000@sophia.inria.fr.  Accepted contributions will be included in
the informal workshop proceedings, which will be available at the

  As a followup to the workshop, a special issue on logical frameworks
and meta-languages will be published by the Journal of Functional
Programming. Participants will be invited to submit full versions for
this special issue. (See 

  The workshop will be one full day and will be open to all interested

  Program Committee:

    David Basin (Freiburg)            Thierry Coquand (Goteborg)
    Joelle Despeyroux (INRIA, Chair)  Amy Felty (Ottawa)
    Robert Harper (CMU)               Martin Hofmann (Edinburgh)
    Benjamin Pierce (Penn)            Benjamin Werner (INRIA)