Skip to Content.
Sympa Menu

coq-club - [Coq-Club] CFP: Special Issue Journal of Logic and Computation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] CFP: Special Issue Journal of Logic and Computation


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page