Special Issue on Proof Search in Type-theoretic Languages

        *                                                                 *
        *     2nd Call for Papers --- Submission Deadline Extended to     *
        *                             15 September, 1997                  *
        *                                                                 *

	      Special Issue of Theoretical Computer Science (TCS) 
              (Editor-in-Chief: M. Nivat)


              * Proof-search in Type-theoretic Languages * 

              Guest Editors:   
              Didier Galmiche	           David Pym   
              CRIN-CNRS & UHP Nancy 1      Queen Mary & Westfield College
              Nancy, France                University of London 

        Algorithmic proof-search is a fundamental enabling technology 
        throughout artificial intelligence and computer science.    
        There is a long history of work in proof-search in a variety 
        of systems of logic, including classical, intuitionistic, 
        relevant, linear and modal systems, at the propositional, first-  
        and higher-order levels. Such work has ranged from the 
        most abstract to the most practical and has employed 
        the full spectrum of logical techniques, from proof theory, 
        model theory and recursion theory. 

        Recently, there has been a great deal of work on proof-search 
        in type-theoretic languages. Such languages can be thought 
        of as logical frameworks to represent proofs and to formalize 
        connections between proofs and programs. 

        Two recent workshops on "Proof-search in Type-theoretic Languages" 
        (Nancy, 1994 and Rutgers University, NJ, 1996) have provide exchanges 
        of ideas and experiences in topics concerned with proof-search in type
        theory, logical frameworks and their underlying (e.g., classical,
        intuitionistic, linear) logics. 

        Here again, the scope of languages studied and techniques
	employed has been wide, stretching to include algebraic and
	categorical methods.    

        From the computational point of view, the type-theoretic 
        component of logical languages, which may involve 
        propositional, first-order, higher-order or polymorphic 
        assignment regimes, introduces significant challenges for 
        both theoreticians and implementors.  

        *   TOPICS    * 

        Topics of interest include, but are not restricted to:        
	* Natural deduction, sequent calculi systems for
	  type-theoretic languages. Based-on tableaux, matrix or
	  resolution methods for proof-search in type-theoretic

        * Semantic techniques in proof-search. Search vs. deduction as
	  the basis of logic; consequences for model theory 

        * Theorem proving and program development with type-theoretic
	  languages: concepts, techniques, implementation and

        * Logic programming in type-theoretic languages 
          as search-based computation; integration of model-theoretic 
          semantics and imperative aspects of logic programming 

        * Operational semantics and proof theory of search-based
          Denotational semantics and model theory of search-based

        * Complexity of search problems in type-theoretic languages; 
          comparisons with non-type-theoretic systems.

        * SUBMISSIONS * 
        Prospective contributors are warmly invited to contact 
        either, or both, of the guest editors (see addresses below) 
        to discuss the suitability of topics and papers. 

        The submissions should satisfay the usual standards of
        scholarship, originality and high-quality of the TCS journal.

	The new submission deadline is  * 15 September, 1997 * 

         Please submit either 4 paper copies or, preferably, 
         a postscript file to both of the addresses given


                      Didier Galmiche, CRIN-CNRS & UHP Nancy 1, 
                                       Batiment LORIA, Campus
                                       Scientifique, B.P. 239,
                                       54506 Vandoeuvre-les-Nancy
                                       Tel: +33 (0)3 83 59 20 15
                                       Fax: +33 (0)3 83 41 30 79  
				       URL: http://www.loria.fr/~galmiche     

                       David Pym,      Department of Computer Science, 
                                       Queen Mary and Westfield College, 
                                       University of London, 
                                       Mile End Road, 
                                       London E1 4NS, 
                                       England U.K. 

                                       Tel: +44 (0)171 975 5237  
                                       Fax: +44 (0)181 980 6533 
				       URL: http://www.dcs.qmw.ac.uk/~pym       

Please address administrative mail regarding the lambda Prolog mailing list to
lprolog-request@cis.upenn.edu.  See http://www.cis.upenn.edu/~dale/lProlog.