* TCS Special Issue: Proof-search in Type-theoretic Languages.
@ 1997-04-24 18:22 categories
0 siblings, 0 replies; only message in thread
From: categories @ 1997-04-24 18:22 UTC (permalink / raw)
To: categories
Date: Tue, 22 Apr 1997 16:47:40 +0100 (BST)
From: David Pym <pym@dcs.qmw.ac.uk>
[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
------------------------------------------------------------------------------
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~1997-04-24 18:22 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1997-04-24 18:22 TCS Special Issue: Proof-search in Type-theoretic Languages categories
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).