[Prev][Next][Index][Thread]

IMLA 02 Second Call for Papers


  FLoC'2002 Workshop

  IMLA 2: Intuitionistic Modal Logic and Applications '02
          http://floc02.diku.dk/IMLA/

  July 26, 2002
  Copenhagen, Denmark


BACKGROUND

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.

The goal of this workshop is to stimulate more systematic study of
constructive
or Intuitionistic Modal Logics and, in parallel of modal type theories. It
aims to
1. bring together two largely parallel communities - computer scientists
with a focus on proof theory and lambda calculi, and logicians and
philosophers with a focus on model theory;
2. bring together theoretically-oriented and the application-oriented
approaches, in the hope of productive interaction.

Topics of interest for papers in the Workshop 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,
      *  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
      *   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


FORMAT

  The workshop will be an informal one-day meeting with two invited
  talks, regular paper presentations, and discussion.


INVITED SPEAKERS

  Giovanni Sambin (Padova, Italy)
  Dana Scott (Pittsburgh, USA)


PUBLICATION

Workshop contributions must be original work that has not yet appeared
elsewhere. If accepted, the authors are expected to present their paper at
the workshop.
Workshop papers will be made available on the  workshop web page and
will  appear  as a technical report  handed out to all workshop
participants.

Authors of accepted papers will be invited to submit
full and revised versions  of the Workshop papers to a special issue of
the Journal of  Logic and Computation, for which there will be a second
round of refereeing.


SUBMISSIONS

All submissions should be single column, use 11 point font, and be at most
15 pages in length, preferably using the LaTeX llnc style. Papers should not
be already published and should not be submitted for simultaneous
publication at another conference or workshop. Either send a .ps or .pdf
file to M.Mendler@dcs.shef.ac.uk <mailto:M.Mendler@dcs.shef.ac.uk>
or post a hard copy to

Michael Mendler
Informatics Theory Group
Faculty of Business and Applied Informatics
University of Bamberg
Feldkirchenstr. 21
D-96047 Bamberg
Germany
by the due date.

IMPORTANT DATES

  IMLA submission deadline: April 5, 2002
  IMLA notification       : May 23, 2002
  IMLA final version      : June 20, 2002

PROGRAMME COMMITTEE

 Natasha Alechina (Nottingham, UK)
 Sergei Artemov (CUNY, USA)
 Johan van Benthem (Amsterdam and Stanford)
 Rajeev Goré (ANU, Australia)
 Jean Goubault-Larrecq (ENS-Cachan, France)
 Michael Mendler (Sheffield ,UK)
 Eugenio Moggi (Genova, Italy)
 Valeria de Paiva (PARC, USA)
 Frank Pfenning (CMU, USA)
 Carsten Schuermann (Yale, USA)
 Alex Simpson (Edinburgh, UK)

ORGANISERS

  Rajeev Gore (ANU, Australia)
  Michael Mendler (Sheffield, UK)
  Valeria de Paiva (PARC, USA)


Workshop webpage:   http://floc02.diku.dk/IMLA/