FLoC '02 - IMLA

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 http://discus.anu.edu.au/~rpg/IMLA02/IMLA02.html.

Description

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

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

Giovanni Sambin, U Padova, Italy
Open truth and closed falsity
Dana Scott, Carnegie Mellon U, USA
Realizability and modality

Program Committee

Natasha Alechina, U Nottingham, UK
Sergei Artemov, City U of New York, USA
Johan van Benthem, U Amsterdam, The Netherlands
Matt Fairtlough, U Sheffield, UK
Rajeev P. Goré, Australian National U
Jean Goubault-Larrecq, ENS Cachan, France
Michael Mendler, U Bamberg, Germany
Eugenio Moggi, U Genova, Italy
Valeria de Paiva, Palo Alto Reseach Center, USA
Frank Pfenning, Carnegie Mellon U, USA
Carsten Schürmann, Yale U, USA
Alex Simpson, U Edinburgh, UK

Organizers

Valeria de Paiva <paiva@parc.xerox.com>, Palo Alto Reseach Center, USA
Michael Mendler <M.Mendler@dcs.shef.ac.uk>, U Bamberg, Germany
Rajeev P. Goré <rpg@arp.anu.edu.au>, Australian National U