[Prev][Next][Index][Thread]
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)
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 satisfay 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 both 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
URL: 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
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.