[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

                     Fourth Internation Workshop on

              Intuitionistic Modal Logic and Applications



                     A LICS'08 affiliated workshop

                Pittsburgh, Pennsylvania, June 23, 2008

Constructive modal logics and type theories are of increasing foundational and 
practical relevance in computer science. 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.

This workshop will bring together designers, implementers, and users to discuss 
all aspects of intuitionistic modal logics and type theories.  Topics 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, foundations of security, 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

The workshop continues a series of previous LICS-affiliated workshops, which 
were held as part of FLoC'99, Trento, Italy and of FLoC'02, Copenhagen, Denmark.

We solicit submissions on work in progress and on more mature results. 
Submissions should be extended abstracts of 5-10 pages sent in PostScript or 
PDF format to the program co-chair at [EMAIL PROTECTED]<mailto:[EMAIL 


Submission: April 25, 2008

Notification: May 23, 2008

Final papers due: June 7, 2008

Workshop Date: June 23, 2008

It is planned to publish workshop proceedings as Electronic Notes in 
Theoretical Computer Science (ENTCS) or in CEURS, to be decided. Authors please 
use the generic ENTCS macro package at http://www.math.tulane.edu/~entcs.


Gavin Bierman (Microsoft, UK)

Valeria de Paiva (PARC, USA)

Michael Mendler (Bamberg, DE)

Aleks Nanevski (Microsoft, UK)

Brigitte Pientka (McGill, CA)

Eike Ritter (Birmingham, UK)


Frank Pfenning (CMU, USA)

Torben Brauner (Roskilde, DK)


Valeria de Paiva                 Aleks Nanevski

PARC, Palo Alto Research Center  Microsoft Research


Reply via email to