The series of workshops on Intuitionistic Modal Logic and Applications (IMLA) owes its existence to the hope that philosophers, mathematical logicians and computer scientists would share information and tools when investigating intuitionistic modal logics and modal type theories, if they knew of each other’s work.
More than ten years have passed since the retrospective view of de Paiva, Gore, and Mendler , and progress in the area of constructive modal logic has been slow and getting slower. It is our view that differences in the outlook of the various groups of scholars interested in the topic, differences that were once fruitful, now are responsible for a tendency for the new work to be driven by technical issues that have not had wide interest, leading to compartmentalisation and waning interest in the IMLA’s big tent. Work on modal type theories seems to have been pursued in narrow tracts. For instance, much work in the
symposium on Principles of Programming Languages (POPL), in specific type systems could be considered work in applied constructive modal logic, but this aspect is neglected because it is not considered useful or productive. Generally speaking, topic specialists have stopped expecting outsiders to say anything of
interest to them, so they do not make the effort to say anything of interest to outsiders.
This is a shame, since there are big questions in the field that hold broad interest that have not been answered and that might benefit from the breadth that once characterised the field. To this end, we offer a new retrospective of the field, aimed at giving a sense of the dynamics that have driven compartmentalisation, and make the case for reengagement with certain broad issues which offer all parties the hope of systematic theories that are much better suited to all of their needs.