Workshop on

TYPE-THEORETIC LANGUAGES: PROOF-SEARCH AND SEMANTICS
(in conjunction with CADE-17)
CMU Pittsburgh, Pennsylvania, 16 or 21 June, 2000

A one day workshop on Type-Theoretic Languages: Proof Search and Semantics will be held in June 2000 in conjunction with the CADE-17 (17th Conference on Automated DEduction, CMU Pittsburgh, Pennsylvania, June 17-20, 2000). Hardcopies of the preliminary proceedings will be distributed at the workshop.

Final proceedings will be published 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 settings. The focus of this workshop is on proof-search, with a specific interest on semantic aspects of, and semantics approaches to, type-theoretic languages and their underlying logics (e.g., classical, intuitionistic, linear, substructural). Such languages can be seen as logical frameworks for representing proofs and in some cases formalize connections between proofs and programs that support program-synthesis.

The theory of proof-search has developed mostly along proof-theoretic lines but using many type-theoretic techniques. The utility of type-theoretic methods suggests that semantic methods of the kind found to be valuable in the semantics of programming languages should be useful in tackling the main outstanding difficulty in the theory of proof-search, i.e., the representation of intermediate stages in the search for a proof. An adequate semantics would represent both the space of searches and the space of proofs and give an account of the recovery of proofs (which are extensional objects) from searches (which are more intensional objects). It would distinguish between different proof-search strategies and permit analyses of their relative merits.

The objective of the workshop is to provide a forum for discussion between, on the one hand, researchers interested in all aspects of proof-search in type theory, logical frameworks and their underlying (e.g., classical, intuitionistic, substructural) logics and, on the other, researchers interested in the semantics of computation.

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

Foundations of proof-search in type-theoretic languages (sequent calculi, natural deduction, logical frameworks, etc.);
Systems, methods and techniques related to proof construction or to counter-models generation (tableaux, matrix, resolution, semantic techniques, proof plans, etc.);
Decision procedures, strategies, complexity results;
Logic programming as search-based computation, integration of model-theoretic semantics, semantic foundations for search spaces;
Computational models based on structures as games and realizability;
Proof synthesis vs program synthesis and applications, equational theories and rewriting;
Applications of proof-theoretic and semantics techniques to the design and implementation of theorem provers.

Calls

Call for contributions (.ps file)

Submissions

Researchers interested in presenting their works are invited to send an extended abstract (up to 10-12 pages)} by e-mail submissions of Postscript files to the Programme Chair (Didier.Galmiche@loria.fr) before April 1, 2000. Papers will be reviewed by peers, typically members of the programme committee. The cover page should include a return mailing address and, if possible, an electronic mail address and a fax number.

Programme Chair

Didier Galmiche 
LORIA UMR 7503 & Universite Henri Poincare 
Campus Scientifique, B.P. 239 
54506 Vandoeuvre-les-Nancy, France 
email: Didier.Galmiche@loria.fr
fax: [+33] 03 83 41 30 79 
URL: http://www.loria.fr/~galmiche

Program Committee

D. Galmiche (LORIA - UHP, Nancy)
P. Lincoln (SRI, Stanford)
F. Pfenning (Carnegie Mellon University, Pittsburgh)
D. Pym (Queen Mary & Westfield College, London)
J. Smith (Chalmers University, Goteborg)

Important dates: