
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 metalogics for reasoning about a variety of
computational phenomena.
Theoretical and methodological issues center around the question of how
the prooftheoretic strengths of constructive logics can best be
combined with the modeltheoretic 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 LICSaffiliated workshops, entitled "Intuitionistic Modal Logic and Applications (IMLA)" which were held as part of FLoC'99, Trento, Italy and of FLoC2002, Copenhagen, Denmark.
Preliminary Program:
All talks will be in the School of CTI, DePaul University, 243 South Wabash Ave.
The room is TBA. 
9:40 

Opening
Frank Pfenning, Carnegie Mellon University 
9:45 

INVITED TALK: Checking Properties of Pointer Programs
David Walker, Princeton University 
10:30 

Coffee Break 
11:00 

A Modal Calculus for Named Control Effects
Aleksandar Nanevski, Carnegie Mellon University 
11:30 

A Computational Interpretation of Classical S4 Modal Logic
Chunchieh Shan, Harvard University 
12:00 

A Term Calculus for Dual Intuitionistic Logic
Gianluigi Bellin, University of Verona & QMW College, University of London 
12:30 

Lunch 
14:00 

INVITED TALK: Intuitionistic Modal Logic: observations from algebra and duality
Yde Venema, University of Amsterdam 
14:45 

Labeling Sequents: motivations and applications
Patrick Girard, Stanford University 
15:15 

On the inferential role semantics of modal logic
Charles Stewart, Dresden University of Technology 
15:30 

Coffee Break 
16:00 

SPECIAL CONTRIBUTION: Gödel's Interpretation of Intuitionism
William W. Tait, University of Chicago 
16:45 

Constructive Description Logics: work in progress
Valeria de Paiva, PARC 
17:00 

End 
Invited Speakers:
David Walker, Princeton University Checking Properties of Pointer Programs
Yde Venema, University of Amsterdam  Intuitionistic Modal Logic: observations from algebra and duality
Important Dates:
Workshop Date: 30 June 2005
LICS'05 Dates: 2629 June 2005
PASSED:
Early Registration Deadline: 20 May 2005
Submission Deadline: 17 April 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 coinductive types, higherorder 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. 