[Prev][Next][Index][Thread]

CFP CADE-17 Workshop "Type-theoretic Languages: Proof search and Semantics"



                        CALL FOR CONTRIBUTIONS


                             Workshop on

              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
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
the following:

- 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. 
 

SUBMISSIONS

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: 
http://www.loria.fr/~galmiche/TTL-PSS00.html


PROGRAMME COMMITTEE:

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) 

IMPORTANT DATES

Deadline for submissions:           1 April, 2000.
Notification of acceptance:         1 May, 2000.
Workshop date:                      June 16 or 21, 2000.

INFORMATION

Programme 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/TTL-PSS00.html