IMLA 2002

Intuitionistic Modal Logic and Aplications
Copenhagen, Denmark, July 26th, 2002
Affiliated with LICS 2002

Workshop web page

The main IMLA02 page is at


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 Coq and LEGO. 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. 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 philosphers with a focus on model theory;
  2. bring together theoretically-oriented and the application-oriented approaches, in the hope of productive friction.
Theoretical / methodological issues centre around the question of how the proof-theoretic strengths of constructive logics can best be combined with the model-theoretic 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 co-inductive types, higher-order abstract syntax, strong functional programming
  • Curry-Howard correspondence between computational lambda calculi and computational 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

IMLA'99 was held as part of the previous FLoC.

Invited speakers

Program Committee