IMLA2017

The 7th Workshop on Intuitionistic Modal Logic and Applications (IMLA) will be held in association with ESSLLLI 2017, which will take place at the University of Toulouse (France), 17-28 July, 2017.

The workshop continues a series of previous workshops which were held as part of FLoC1999, Trento, Italy, of FLoC2002, Copenhagen, Denmark, as part of LiCS2005, Chicago, USA and LiCS2008,

Pittsburgh, USA and as part of the 14th Congress of Logic, Methdology and Philosophy of Science, Nancy, France, 25 July, 2011 and as part of Unilog 2013 in Rio de Janeiro, Brazil.

Constructive modal logics and type theories are of increasing foundational and practical relevance in computer science.

Applications of constructive modal logics are in type disciplines for programming languages, meta-logics for reasoning about a variety of computational phenomena

and explanatory frameworks in philosophical logic. The workshop aims at developing and explaining theoretical and methodological issues centered 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 of which modal connectives with associated laws or proof rules capture computational phenomena accurately and at the right level of abstraction.

Topics of interest

Topics of interest of this workshop include but are not limited to:

• • applications of intuitionistic necessity and possibility

  • (co)monads and strong (c0)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) or EPTCS.

Furthermore, accepted papers might be invited to submit extended and revised versions to a special issue of a journal, to be decided.

Organizing Institutions: