coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: michael.mendler AT wiai.uni-bamberg.de
- To: appsem AT cs.chalmers.se, categories AT mta.ca, comlab AT comlab.ox.ac.uk, compulog-deduction AT cs.bham.ac.uk, coq-club AT pauillac.inria.fr, eacsl AT dimi.uniud.it, fsdm AT svrc.uq.edu.au, igpl AT doc.ic.ac.uk, info-hol AT ultimate.cs.byu.edu, isabelle-users AT cl.cam.ac.uk, lfcs-interest AT dcs.ed.ac.uk, lics-request AT dcs.ed.ac.uk, linear AT cs.stanford.edu, logic AT CS.Cornell.EDU, lprolog AT cs.umn.edu, proof-sci AT cs.chalmers.se, pvs AT csl.sri.com, qed AT mcs.anl.gov, theorem-provers AT ai.mit.edu, theory AT dcs.st-and.ac.uk, theory-a AT listserv.nodak.edu, theorynt AT listserv.nodak.edu, types-wg AT durham.ac.uk, types AT dcs.gla.ac.uk, types AT cis.upenn.edu, appsem AT cs.chalmers.se, appsem AT cs.chalmers.se, categories AT mta.ca
- Cc: michael.mendler AT wiai.uni-bamberg.de, rpg AT discus.anu.edu.au, Valeria.dePaiva AT parc.com
- Subject: [Coq-Club] CFP: Special Issue Journal of Logic and Computation
- Date: Mon, 18 Nov 2002 13:30:42 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Priority: normal
[... apologies for multiple copies ... ]
**************************************************************************
*** JOURNAL OF LOGIC AND COMPUTATION
***
***
***
***
SPECIAL ISSUE ON
***
*** MODALITIES IN CONSTRUCTIVE LOGICS AND ***
*** TYPE THEORIES
***
***
***
*** FIRST CALL FOR PAPERS
***
***
***
***************************************************************************
TOPIC
Constructive and modal logics
are of foundational and practical
relevance to Computer Science.
Constructive logics are used as type
disciplines for programming
languages, as metalogics for
denotational semantics, in
the paradigm of program extraction from
proofs and for interactive
proof development in automated deduction
systems such as Agda, Coq,
Twelf, Isabelle, HOL, NuPrl and
Plastic. Modal logics like
temporal logics, dynamic logics and
process logics are used in
industrial-strength applications as
concise formalisms for capturing
reactive behaviour. Although
constructive and modal frameworks
have typically been investigated
separately, a growing body
of published work shows that both
paradigms can (and should)
be fruitfully combined.
This special issue aims
* to give a state-of-the-art snapshot of recent advances in the
study of constructive modalities,
* to put equal focus on the theory-oriented as well as the
application-oriented approaches, and
* to bring together two largely parallel communities - computer
scientists with a focus on proof theory and lambda calculi, and
logicians and philosphers with a focus on model theory.
Topics of interest for contributions
to the journal issue include,
but are not limited to:
* applications of intuitionistic necessity or possibility,
strong monads, or evaluation modalities,
* use of modal type theory to formalize mechanisms of
abstraction and refinement, or to manage intensional
concepts (computer science, linguistics, or the philosophy of
science) in a rigorous deductive fashion
* applications of constructive modal logic and modal type
theory to formal verification, abstract interpretation, and
program analysis and optimization
* applications of modal types to integration of inductive and
co-inductive types, higher-order abstract syntax, strong
functional programming
* computational aspects of the Curry-Howard correspondence
between lambda calculi and logics
* extensions of this correspondence by other modalities or
quantifiers
* models of constructive modal logics such as algebraic,
categorical, Kripke, topological, realizability
interpretations, games semantics
* notions of proof for constructive modal logics
* extraction of constraints or programs, nonstandard
information extraction techniques
* proof search in constructive modal logic and implementations
of it
SUBMISSIONS
Submissions must be original work,
which has not been previously
published in a journal and is not
being considered for publication
elsewhere. Manuscripts should be type
written on one side only with
wide margins, and not longer than
30 pages. The typing should be
double-spaced. Pages should be numbered
consecutively. A title page
must include: full title, authors'
full names and affiliations, and
the address to which correspondence
and proofs should be sent. Where
possible, e-mail address and telephone
number should be included. This
should be followed by an abstract
of approximately 300 words and five
key words for indexing.
Send a .ps or .pdf file to michael.mendler AT wiai.uni-bamberg.de
or post a hard copy to
Michael Mendler
Informatics Theory Group
Faculty of Business and
Applied Informatics
The Otto-Friedrich University
of Bamberg
Feldkirchenstr. 21
D-96045 Bamberg
Germany
by the due date.
IMPORTANT DATES
Submission
: February 28, 2003
Notification
: April 30, 2003
Final version
: June 11, 2003
CHIEF EDITOR
Dov Gabbay (King's College,
London)
GUEST EDITORS
Rajeev Gore (ANU, Australia)
Michael Mendler (Bamberg University,
DE)
Valeria de Paiva (PARC, USA)
--
Prof. Michael Mendler, PhD
Universität Bamberg
Professur für Grundlagen der
Informatik
Bamberg University
Faculty of Business and Applied Informatics
Informatics Theory Group
Feldkirchenstraße 21
D-96045 Bamberg
Germany
Phone: ++49
951 863-2828
Fax:
++49 951 863-1200
E-Mail: michael.mendler AT wiai.uni-bamberg.de
WWW: http://www.uni-bamberg.de/wiai/gdi
- [Coq-Club] CFP: Special Issue Journal of Logic and Computation, michael . mendler
Archive powered by MhonArc 2.6.16.