Program Committee:
Natasha Alechina (Nottingham, UK)
Frank Pfenning (CMU, USA)
Carsten Schuermann (Yale, USA)
Alex Simpson (Edinburgh, UK)
Valeria de Paiva (PARC, USA)
Dr. Valeria de Paiva
PARC, Palo Alto Research Center
Email: paiva at parc . xerox . com
Prof. Frank Pfenning
Department of Computer Science
Carnegie Mellon University
Email: fp at cs . cmu . edu
Intuitionistic Modal Logics and Applications Workshop (IMLA '05)
June 30, 2005
A Logic in Computer Science Conference affiliated workshop
Constructive modal logics and type theories are of increasing foundational and practical relevance in computer science. Sample applications are in type disciplines for programming languages, and meta-logics for reasoning about a variety of computational phenomena.
Theoretical and methodological issues center around the question of how the proof-theoretic strengths of constructive logics can best be combined with the model-theoretic strengths of modal logics. Practical issues center around the question which modal connectives with associated laws or proof rules capture computational phenomena accurately and at the right level of abstraction.
The workshop continues a series of previous LICS-affiliated workshops, entitled "Intuitionistic Modal Logic and Applications (IMLA)" which were held as part of FLoC'99, Trento, Italy and of FLoC2002, Copenhagen, Denmark.
Call for Papers:
Submission Deadline: 17 April 2005
Notification of authors accepted papers: 9 May 2005
Workshop Date: 30 June 2005
LICS'05 Dates: 26-29 June 2005
Topics of interest for papers in the workshop include, but are not limited to:
- applications of intuitionistic necessity and possibility
- monads and strong monads
- constructive belief logics and type theories
- applications of constructive modal logic and modal type theory to formal verification, abstract interpretation, and program analysis and optimization
- modal types for integration of inductive and co-inductive types, higher-order abstract syntax, strong functional programming
- models of constructive modal logics such as algebraic, categorical, Kripke, topological, and realizability interpretations
- notions of proof for constructive modal logics
- extraction of constraints or programs from modal proofs
- proof search methods for constructive modal logics and their implementations
Publication Plans
It is planned to publish workshop proceedings as Electronic Notes in Theoretical Computer Science (ENTCS). Furthermore, accepted papers might
be invited (in revised and extended form) for a special issue of a
journal.
Authors should go to the ENTCS Macro Home Page http://www.math.tulane.edu/~entcs and download the generic ENTCS macro package linked near the top of the page. You also should download a copy of the file prentcsmacro.sty that's linked in the listing for the IMLA workshop in the table at the bottom of the page. You should substitute this file for the file entcsmacro.sty that's included in the generic package, and then use the file example.tex as a template for your submission.