ILMA: FLoC Satellite Workshop

on

Intuitionistic Modal Logics and Applications

held at

Copenhagen, Denmark, July 26, 2002

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. 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 theoretically-oriented and the application-oriented approaches, in the hope of productive interaction.

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