Last CFP CADE-12 Workshop on Proof Search in Type-theoretic Languages



                       Nancy, France, June 26, 1994

This workshop will focus on the problems of proof search in
type-theoretic languages.  Such languages are used as logical
frameworks for representing proofs and, in some cases, formalize
connections between proofs and programs that support program
The purpose of the workshop is to discuss recent results
in, and to establish and publicize a research agenda for, proof search
in type theories and their use in the formal development of correct
proofs and programs.


The workshop is intended to bring together researchers interested in  
all aspects of proof search in type-theoretic languages, including but 
not limited to the following topics: 

* foundations of proof search in type theory frameworks 

* techniques and concepts related to proof construction 
  and related analysis  

* proof synthesis vs program synthesis (applications, specific methods)

* environments for formal proof development in type-theoretic frameworks


The workshop is held, during one full day (June 26, 1994),
in conjunction with CADE-12 Conference). Attendance is by invitation
only: authors of accepted submissions will be invited. Informal
proceedings will be supplied by the CADE organizing committee. 


Researchers interested in presenting their work are invited to send an
extended abstract (5-7 pages) to each of the organizers named below.
Researchers interested in attending the workshop (without giving a
presentation) should send a position paper (1-2 pages) presenting 
their interest. 
e-mail submissions (*.dvi or *.ps files) are requested 
(hardcopies are also accepted) before April 15, 1994. Notification of 
acceptance and invitations to the workshop will be issued by 
May 5, 1994. Material to be handed out at the workshop should be 
received in final form before May 24, 1994. 

All submissions and information requests should be sent to the 
workshop organizers: 

Didier Galmiche                       Lincoln Wallen 
CRIN-CNRS & INRIA Lorraine            Computing Laboratory 
Campus Scientifique, B.P. 239         University of Oxford 
54506 Vandoeuvre-les-Nancy,           Parks Road, Oxford OX1 3QD, 
France                                U.K. 
email: Didier.Galmiche@loria.fr       email: Lincoln.Wallen@prg.ox.ac.uk 
fax: [+33] 83 41 30 79                fax: [+44] 865 27 38 39 


Deadline for submission:       April 15, 1994 
Notification of acceptance:    May    5, 1994 
Abstract final version:        May   24, 1994 

Program Committee:

D. Galmiche (CRIN-CNRS & INRIA, Nancy) 
L. Helmink  (Philips Research Laboratories, Eindhoven)
F. Pfenning (Carnegie Mellon University, Pittsburgh) 
S. Thompson (University of Kent) 
L. Wallen   (University of Oxford)