CFP CADE-17 Workshop "Type-theoretic Languages: Proof search and Semantics"
CALL FOR CONTRIBUTIONS
TYPE-THEORETIC LANGUAGES: PROOF-SEARCH AND SEMANTICS
(in conjunction with CADE-17)
CMU Pittsburgh, Pennsylvania
16 or 21 June, 2000
DEADLINE FOR SUBMISSION: 1 April, 2000.
A one day workshop on "Type-Theoretic Languages: Proof Search and
Semantics" will be held in June 2000 in conjunction with the 17th
Conference in Automated DEduction (http://www.research.att.com/conf/cade/).
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
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
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
- 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.
Researchers interested in presenting their works are invited to send an
extended abstract (up to 10 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.
Additional information will be available through WWW address:
D. Galmiche (LORIA & UHP, Nancy) - Programme Chair
P. Lincoln (SRI, Stanford)
F. Pfenning (CMU, Pittsburgh)
D. Pym (Queen Mary & Westfield College, Univ. of London)
J. Smith (Chalmers Univ., Goeteborg)
Deadline for submissions: 1 April, 2000.
Notification of acceptance: 1 May, 2000.
Workshop date: June 16 or 21, 2000.
LORIA - CNRS & UHP Nancy I
Phone: +33 3 83 59 20 15
Fax: +33 3 83 41 30 79