Program Committee:

Natasha Alechina (Nottingham, UK)
Frank Pfenning (Carnegie Mellon, USA)
Carsten Schuermann (Yale, USA)
Alex Simpson (Edinburgh, UK)
Valeria de Paiva (PARC, USA)

Contact Information:

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

Important Dates:

Workshop Date:
30 June 2005

LICS'05 Dates:
26-29 June 2005

Registration and Accommodations

LICS/IMLA Registration:
https://securestore.cti.depaul.edu/LICS2005/

Local Information:
http://lics.cs.depaul.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.

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
Chun-chieh 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: 26-29 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 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.
   
Back to the LICS 05 web page