

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 industrialstrength 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. 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

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;

bring together the theoreticallyoriented and the
applicationoriented approaches, in the hope of productive
interaction.
Theoretical / methodological issues centre around the question of
how the prooftheoretic strengths of constructive logics can best
be combined with the modeltheoretic strengths of modal logics. Two
basic questions are thus "what is the right notion of proof?" and
"what is the right way of making a given modal logic constructive?"
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
coinductive types, higherorder abstract syntax, strong
functional programming

computational aspects of the CurryHoward 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

