[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 Didier.Galmiche@loria.fr 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. pym@dcs.qmw.ac.uk Tel: +44 (0)171 975 5237 Fax: +44 (0)181 980 6533 WWW: http://www.dcs.qmw.ac.uk/~pym ------------------------------------------------------------------------------