[TYPES/announce] IMLA11: Call for Papers

[Valeria de Paiva]

                  Fifth International Workshop on
             Intuitionistic Modal Logic and Applications
                              (IMLA'11)

             (http://www.agents.cs.nott.ac.uk/events/imla11)

 A 14th Logic, Methodology and Philosophy of Science affiliated workshop
                           Nancy, France, July, 2011

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,part of LiCS2005, Chicago, USA and LiCS2008,
Pittsburgh, USA.

We solicit submissions on work in progress and on more mature results.
Submissions should be extended abstracts of 5-10 pages sent in
PDF format to either or both of the  co-chairs nza at cs.nott.ac.uk,
valeria.depaiva at gmail.com.

IMPORTANT DATES:

Submission: December 15, 2010
Notification: January  15, 2011
Final papers due: March 31, 2011
Workshop Date: TBA

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.


INVITED SPEAKERS include:

Michael Mendler (Bamberg, DE)
Brian Logan (Nottingham, UK)
Lutz Strassburger (LIX, FR)

PROGRAM COMMITTEE

Nick Benton (Microsoft, UK)

Natasha Alechina (Nottingham, UK)

Didier Galmiche (Nancy, FR)

Hermann Hausler (PUC-RJ, BR)

Valeria de Paiva (Birmingham, UK)


CONTACTS

Natasha Alechina (nza at cs.nott.ac.uk)
Valeria de Paiva (valeria.depaiva at gmail.com)


--
Valeria de Paiva
http://www.cs.bham.ac.uk/~vdp/
http://valeriadepaiva.org/www/



-- 
Valeria de Paiva
http://www.cs.bham.ac.uk/~vdp/
http://valeriadepaiva.org/www/