coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] IMLA'08: Call for Papers

From: Aleks Nanevski <aleksn AT microsoft.com>
To: "types AT cis.upenn.edu" <types AT cis.upenn.edu>, "pieper AT mcs.anl.gov" <pieper AT mcs.anl.gov>, "asl AT vassar.edu" <asl AT vassar.edu>, "lics-request AT dcs.ed.ac.uk" <lics-request AT dcs.ed.ac.uk>, "ftp-ws-community AT mpi-sb.mpg.de" <ftp-ws-community AT mpi-sb.mpg.de>, "rewriting AT ens-lyon.fr" <rewriting AT ens-lyon.fr>, "kgs AT logic.tuwien.ac.at" <kgs AT logic.tuwien.ac.at>, "theorem-provers AT ai.mit.edu" <theorem-provers AT ai.mit.edu>, "theorynt AT listserv.nodak.edu" <theorynt AT listserv.nodak.edu>, "qed AT mcs.anl.gov" <qed AT mcs.anl.gov>, "aisb AT cogs.sussex.ac.uk" <aisb AT cogs.sussex.ac.uk>, "behavior AT cs.ucsd.edu" <behavior AT cs.ucsd.edu>, "caml-list AT pauillac.inria.fr" <caml-list AT pauillac.inria.fr>, "categories AT mta.ca" <categories AT mta.ca>, "ccl AT ps.uni-sb.de" <ccl AT ps.uni-sb.de>, "clp AT comp.nus.edu.sg" <clp AT comp.nus.edu.sg>, "comlab AT comlab.ox.ac.uk" <comlab AT comlab.ox.ac.uk>, "complog AT cs.nmsu.edu" <complog AT cs.nmsu.edu>, "compulognet-parimp AT dia.fi.upm.es" <compulognet-parimp AT dia.fi.upm.es>, "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>, "dbworld AT cs.wisc.edu" <dbworld AT cs.wisc.edu>, "facs AT lboro.ac.uk" <facs AT lboro.ac.uk>, "formal-methods AT cs.uidaho.edu" <formal-methods AT cs.uidaho.edu>, "info-hol AT cs.uidaho.edu" <info-hol AT cs.uidaho.edu>, "isabelle-users AT cl.cam.ac.uk" <isabelle-users AT cl.cam.ac.uk>, "it-announce AT cs.usyd.edu.au" <it-announce AT cs.usyd.edu.au>, "kbcsl AT uni-paderborn.de" <kbcsl AT uni-paderborn.de>, "ki-inf AT uni-koblenz.de" <ki-inf AT uni-koblenz.de>, "kr AT kr.org" <kr AT kr.org>, "lfcs-interest AT dcs.ed.ac.uk" <lfcs-interest AT dcs.ed.ac.uk>, "logic-list AT Helsinki.FI" <logic-list AT Helsinki.FI>, "mizar-forum AT mizar.uwb.edu.pl" <mizar-forum AT mizar.uwb.edu.pl>, "prog-lang AT diku.dk" <prog-lang AT diku.dk>, "pvs AT csl.sri.com" <pvs AT csl.sri.com>, "softtech AT cs.uu.nl" <softtech AT cs.uu.nl>, "stp AT dcs.gla.ac.uk" <stp AT dcs.gla.ac.uk>, "theory AT dcs.st-and.ac.uk" <theory AT dcs.st-and.ac.uk>, "theory-logic AT cs.cmu.edu" <theory-logic AT cs.cmu.edu>, "om-announce AT openmath.org" <om-announce AT openmath.org>, "csp AT carlit.toulouse.inra.fr" <csp AT carlit.toulouse.inra.fr>, "acl2 AT cs.utexas.edu" <acl2 AT cs.utexas.edu>, "aiia AT di.unito.it" <aiia AT di.unito.it>, "dl AT dl.kr.org" <dl AT dl.kr.org>, "members AT fmeurope.org" <members AT fmeurope.org>
Subject: [Coq-Club] IMLA'08: Call for Papers
Date: Mon, 11 Feb 2008 17:24:15 +0000
Accept-language: en-US
Acceptlanguage: en-US
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

                     Fourth Internation Workshop on
              Intuitionistic Modal Logic and Applications
                               (IMLA'08)

              (http://www.cs.bham.ac.uk/~vdp/IMLA08.html)

                     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
aleksn AT microsoft.com.

IMPORTANT DATES:

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.

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)

INVITED SPEAKERS:

Frank Pfenning (CMU, USA)
Torben Brauner (Roskilde, RK)

CONTACTS

Valeria de Paiva                 Aleks Nanevski
PARC, Palo Alto Research Center  Microsoft Research
paiva AT parc.xeroc.com

aleksn AT microsoft.com

[Coq-Club] IMLA'08: Call for Papers, Aleks Nanevski