[... apologies for multiple copies ... ] ------------------- WORKSHOP ANNOUNCEMENT ----------------------- *** FIRST 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, dynami= c 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 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 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 no= t 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 Dr Michael Mendler The Department of Computer Science Regent Court 211 Portobello Street Sheffield S1 4DP UNITED KINGDOM 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 (Cornell, USA) Johan van Benthem (Amsterdam and Stanford) Rajeev Gor=E9 (ANU, Australia) Jean Goubault-Larrecq (ENS-Cachan, France) Michael Mendler (Sheffield ,UK) Eugenio Moggi (Genova, Italy) Valeria de Paiva (Xerox 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/