[ 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