Subject: TCS Special Issue: Proof-search in Type-theoretic Languages.

From: categories <[email-masked]>
Date: Thu, 24 Apr 1997 15:22:50 -0300 (ADT)

Date: Tue, 22 Apr 1997 16:47:40 +0100 (BST)
From: David Pym <[email-masked]>

[Apologies for multiple copies of this message.]

Dear Colleague,
 
This message is to remind you that a special issue of TCS dedicated to
the topic "Proof-search in type-theoretic languages" has been
announced, with Didier Galmiche and I as guest editors. Following 
some requests, we have delayed the submission deadline. 

So, please find enclosed the corresponding last call for papers. 
The new (and firm) submission deadline is 15 September, 1997.

Prospective contributors are warmly invited to contact 
either of the guest editors to discuss the suitability of topics and
papers. The submissions should satisfy the usual standards of
scholarship, originality and high-quality of the TCS journal. 

Kind regards, 

	David Pym  

------------------------------------------------------------------------------

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

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

              on 

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

        * 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
	  experimentation   

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

          Denotational semantics and model theory of search-based
          computation.

        * 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 satisfy the usual standards of
        scholarship, originality and high-quality of the TCS journal.

 	* SUBMISSION DEADLINE 	
                                        ********************** 
	The new submission deadline is  * 15 September, 1997 * 
                                        **********************

        * SUBMISSION FORMAT 
              
         Please submit either 4 paper copies or, preferably, 
         a postscript file to either of the addresses given
         below.  

        * SUBMISSION ADDRESSES 

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

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

                                       [email-masked] 
                                       Tel: +44 (0)171 975 5237  
                                       Fax: +44 (0)181 980 6533 
				       WWW: http://www.dcs.qmw.ac.uk/~pym      

------------------------------------------------------------------------------