coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] CFP: Intuitionistic Modal Logic and Applications (IMLA'05)

From: Frank Pfenning <Frank_Pfenning AT fp.logosphere.cs.cmu.edu>
To: lics-request AT dcs.ed.ac.uk, types AT cis.upenn.edu, theorem-provers AT ai.mit.edu, pt AT janeway.inf.tu-dresden.de, types-wg AT durham.ac.uk, appsem AT cs.chalmers.se, linear AT cs.stanford.edu, lprolog AT cs.umn.edu, proof-sci AT cs.chalmers.se, coq-club AT pauillac.inria.fr, isabelle-users AT cl.cam.ac.uk, pvs AT csl.sri.com, linear-all AT iml.univ-mrs.fr
Subject: [Coq-Club] CFP: Intuitionistic Modal Logic and Applications (IMLA'05)
Date: Tue, 15 Feb 2005 11:09:56 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

                     Third Internation Workshop on
              Intuitionistic Modal Logic and Applications
                               (IMLA'05)

                   http://www.cs.cmu.edu/~fp/imla05/

                     A LICS'05 affiliated workshop
                    Chicago, Illinois, June 30, 2005

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.

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, 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 FLoC2002,
Copenhagen, Denmark.

We solicit submissions on work in progress and on more mature results.
Submissions should be extended abstracts of 5-10 pages and sent in
PostScript or PDF format to the program co-chair at
fp AT cs.cmu.edu

IMPORTANT DATES:

  Submission: April 17, 2005
  Notification: May 9, 2005
  Workshop Date: June 30, 2005

PROGRAM COMMITTEE:

  Natasha Alechina (Nottingham, UK)
  Frank Pfenning (co-chair, CMU, USA)
  Carsten Schuermann (Yale, USA)
  Alex Simpson (Edinburgh, UK)
  Valeria de Paiva (co-chair, PARC, USA)

CONTACTS

  Valeria de Paiva                 Frank Pfenning
  PARC, Palo Alto Research Center  Carnegie Mellon University

paiva AT parc.com

fp AT cs.cmu.edu

[Coq-Club] CFP: Intuitionistic Modal Logic and Applications (IMLA'05), Frank Pfenning