IMLA special issue J Log Comp call for papers

IMLA special issue J Log Comp call for papers

[Valeria de Paiva]

Call for Papers: Special Issue of the Journal of Logic and Computation on
Intuitionistic Modal Logics and Applications (IMLA)

Guest Editors: Valeria de Paiva and Natasha Alechina


Constructive modal logics and type theories are of increasing
foundational and practical relevance in computer science. Applications
 in type disciplines for programming languages, and meta-logics for
reasoning about a variety of computational phenomena are plentiful.
Theoretical issues center around the question of
how to combine the proof-theoretic strengths of constructive logics
with the model-theoretic strengths of modal logics. Practical
issues center around the question of which modal connectives with which
associated laws or proof rules capture computational phenomena
accurately and at the right level of abstraction and how to implement
these efficiently.

There have been a series of   LICS-affiliated workshops devoted to the
theme. The first one was held as part of FLoC1999, Trento, Italy, the
second was part  of FLoC2002, Copenhagen, Denmark, the third was
associated with LiCS2005, Chicago, USA and the fourth was associated
with LICS 2008 in Pittsburgh, PA, USA. The last workshop was associated
with the Congress in  Logic and Methodology and Philosophy of Science,
July 2011 in Nancy, France. Two special issues of journals
on the theme have already appeared,  a Mathematical Structures in
Computer Science volume edited by Matt Fairtlough, Michael Mendler and
Eugenio Moggi ( Modalities in type theory) in 2001, and a special
issue of  the Journal of Logic and Computation  in 2004
(Intuitionistic Modal Logics and Application, eds. Valeria de Paiva,
R. Gore ad M. Mendler). A third special issue of Information and
Computation on IMLA, edited by Brigitte Pientka and Valeria de Paiva
is in press.

We are hereby soliciting papers for a further special volume
of the Journal of Logic and Computation, devoted to Intuitionistic Modal
Logics and Applications. We hope to cover the novel applications
presented in the last workshop, but also to include work on
constructive modal logics not presented at the workshop. The proposed
timeline  of events is as follows:
* Papers (under 20 pages long) should be submitted by 31st
January 2012
* Reviews should be provided to authors before the end of May 2012
and the volume should be ready in 2012.

Topics  of interest 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.

Please contact one of the editors (Valeria de Paiva
valeria.depaiva@gmail.com or  Natasha Alechina nza@cs.nott.ac.uk)
if you're not sure that your paper is within the scope of this special
volume. Submissions should be between 10 to 20  pages  long and sent in
PostScript or PDF format to one of the editors, before the 31st
January 2012.



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


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]