CADE-15 Workshop: Proof-search in type-theoretic languages.

["David J. Pym" <pym@dcs.qmw.ac.uk>]

[ Apologies to those who receive this many times through different
channels ]

Dear colleague,

Please find enclosed the Last Call for Contributions for the CADE-15
Workshop on "Proof-search in Type-theoretic Languages", 5th July,
1998 (Lindau, Germany).

Extended Deadline: May 18, 1998.

Information: http://www.loria.fr/~galmiche/cade15-wpsttl.html

Best regards

Didier Galmiche


-----------------------------------------------------------------
                        LAST CALL FOR CONTRIBUTIONS


                            CADE-15 Workshop on

                   PROOF SEARCH IN TYPE-THEORETIC LANGUAGES

                               Lindau, Germany
                                 July 5, 1998


EXTENDED DEADLINE FOR SUBMISSION: May 18, 1998


A one day workshop on "Proof Search in Type-Theoretic Languages"
will be held the 5th July 1998 in conjunction with the 15th Conference
in Automated DEduction (CADE-15, Lindau, Germany).
Attendance is by invitation only: authors of accepted submissions
will be invited. Hardcopies of the preliminary proceedings will be
distributed at the workshop. Proceedings will be published (depending
on the number of high-quality papers) as a volume in Electronic Notes
in Theoretical Computer Science, Elsevier Science Publishers.


TOPICS

Much recent work has been devoted to type theory and its applications
to proof and program development in various logical frameworks.
This workshop focuses on proof search in type-theoretic languages and
their underlying logics(e.g., classical, intuitionistic, linear
logics). Such languages are logical frameworks for representing
proofs and in some cases formalize connections between proofs and
programs that support program synthesis.

The objective of the workshop is to provide an integrated forum for
the presentation of  research and the exchange of ideas and
experiences in proof search in type-theoretic languages and related
logics or logical frameworks.

Topics of interest, in this context, include (but are not restricted
to):

- foundations and semantics of proof search,
- methods, techniques and concepts related to proof construction,
- logic programming as search-based computation, integration of
  model-theoretic semantics,
- proof synthesis vs program synthesis,
- applications,
- equational theories and rewriting,
- decision procedures, complexity results,
- environments for formal proof development.

SUBMISSIONS

Researchers interested in presenting their works are invited to send an
extended abstract (8-10 pages)} by e-mail submissions of Postscript
files to the Program Chair (Didier.Galmiche@loria.fr) before May 14,
1998. Researchers interested in attending the workshop (without giving
a presentation) should send a position paper (1-2 pages) presenting
their interest.
Papers will be reviewed by peers, typically members of the program
committee.
Additional information will be available through WWW address:
http://www.loria.fr/~galmiche/cade15-wpsttl.html


PROGRAM COMMITTEE:

D. Galmiche (LORIA & UHP, Nancy) - Program Chair
P. Lincoln (SRI, Stanford)
F. Pfenning (CMU, Pittsburgh)
D. Pym (Queen Mary & Westfield College, Univ. London)
T. Tammet (Chalmers Univ, Goeteborg)

IMPORTANT DATES

Deadline for submissions:           May 18, 1998
Notification of acceptance:         May 30, 1998
Workshop handouts ready:            June 12, 1998
Workshop date:                      July 5, 1998

INFORMATION

Program Chair

Didier Galmiche
LORIA -  CNRS & UHP Nancy I
B\^atiment LORIA
54506 Vandoeuvre-les-Nancy
France
Phone: +33 3 83 59 20 15
Fax:   +33 3 83 41 30 79
email: Didier.Galmiche@loria.fr
URL: http://www.loria.fr/~galmiche/cade15-wpsttl.html