pitss pic

Program Committee:

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)

Contact Information:

Dr. Valeria de Paiva
PARC, Palo Alto Research Center
Email: paiva at parc  . com

Dr. Aleksandar Nanevski

Microsoft Research
Cambridge, UK
Email: aleks at microsoft . com

Important Dates:

Paper submission: April 25, 2008
Notification: May 23, 2008
Early registration: June 1, 2008
Final papers due: June 7, 2008

Workshop Date:
 23 June 2008

LICS'08 Dates:
24-27 June 2008

Registration is open!

Registration is  handled centrally by CMU for all associated workshops.
All registrations include lunch, refreshment breaks and wireless internet access for each day of attendance. You can book dorm accommodation on campus with conference registration. In addition, LICS and CSF have also reserved blocks of rooms with local hotels.

  • The deadline for early registration is 1 June 2008.
  • The deadline for late online registration is 10 June 2008.
  • After June 10 you must make special arrangements with the conference organizers to register on-site.

Links: Online registration, LICS hotels, CSF hotels

Intuitionistic Modal Logics and Applications Workshop

(IMLA '08)

June 23, 2008

Pittsburgh, Pennsylvania

A Logic in Computer Science Conference affiliated workshop


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.

The workshop continues a series of previous LICS-affiliated workshops,  which were held as part of FLoC1999, Trento, Italy, of FLoC2002, Copenhagen, Denmark and of LiCS2005, Chicago, USA.

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

Preliminary Program:

9:15  Opening

9:25--10:25 Invited talk: Frank Pfenning, Carnegie Mellon University, Pittsburgh, USA

10:25--11:00 Coffee break

11:00--12:15 Session 1

11:00--11:25 Kensuke Kojima and Atsushi Igarashi
                        On Constructive Linear-Time Temporal Logic
11:25--11:50 Rene Vestergaard, Pierre Lescanne and Hiroakira Ono
                        Constructive rationality implies backward induction for conscientious players
11:50--12:15 Simon Kramer
                        Reducing Provability to Knowledge in Multi-Agent Systems

12:15--14:00 Lunch

14:00--15:00 Invited talk: Torben Brauner, Roskilde University, Roskilde, Denmark

15:00--15:30 Coffee break

15:30--17:10 Session 2
15:30--15:55 Neelakantan Krishnaswami
                        A Modal Sequent Calculus for Propositional Separation Logic
15:55--16:20 Didier Galmiche and Yakoub Salhi
                        Calculi for an Intuitionistic Hybrid Modal Logic
16:20--16:45 Kurt Ranalter
                        Two-sequent K and simple fibrations
16:45--17:10 Deepak Garg
                        Principal-Centric Reasoning in Constructive Authorization Logic

Publication Plans

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. We strongly prefer papers  under 10 pages long, excluding appendices.

Please submit (final versions) using EasyChair:


Back to the LICS 08 web page