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  workshops which were held as part of FLoC1999, Trento, Italy, of FLoC2002, Copenhagen, Denmark, as part of LiCS2005, Chicago, USA and LiCS2008Pittsburgh, USA, as part of  the 14th Congress of Logic, Methdology and Philosophy of Science, Nancy, France25 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  in type disciplines for programming languages, meta-logics for reasoning about a variety of computational phenomena and explanatory frameworks in philosophical logic abound. 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 for the applications we are interested in.

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 (co)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
Important Dates

Paper submission deadline: March 29th, 2017
Author notification: April 15th, 2017
[Contribution for Proceedings: 30 May 2017]
Final program [and Proceedings]:   1 June 2017

Scientific and Organizing Committee 
(some to be confirmed)

* Sergei Artemov, (Graduate Center CUNY, USA)
* Valeria de Paiva (Nuance Communications, USA)
* Mario Benevides (COPPE-IM, Rio, BR)
* Elaine Pimentel (DMAT, UFRN, BR)
* Natasha Alechina (Computer Science, University of Nottingham, UK)
* Rosalie Iemhoff (Utrecht University)
* Tudor Protopopescu (Higher School of Economics, Moscow)
* Giuseppe Primiero (Middlesex University London)