RanaldClouston3d ago

8th Workshop on Intuitionistic Modal Logic and Applications (IMLA)
24–25 July 2026, Lisbon, Portugal
Affiliated with the Federated Logic Conference (FLoC 26)
https://sonia-marin.github.io/imla26/

Constructive and intuitionistic modal logics, and their connections with type theory and computation, remain foundationally and practically significant in computer science, logic, and related areas. These include applications in type disciplines, meta-logics for computational phenomena, and explanatory frameworks in philosophical logic. The workshop aims to explore theoretical and methodological issues at the intersection of constructive proof theory and modal semantics, as well as practical questions about which modal connectives and rules best capture computational phenomena at appropriate levels of abstraction.

**Invited speakers**
- Brigitte Pientka (McGill University, Montreal, Canada)
- Ranald Clouston (ANU, Canberra, Australia)
- More to be confirmed.

**Submissions**
We invite abstracts for contributed talks of up to *2 pages* (excluding bibliography). They may describe published work, unpublished work, or work in progress. We especially encourage submissions from students and early-career researchers.

Abstracts should be submitted via the workshop’s submission page:
https://submissions.floc26.org/imla/

(ctd)

#Logic #ModalLogic #CallForAbstracts

IMLA 26

RanaldCloustonJan 21
New preprint! https://arxiv.org/abs/2601.03762 . This is our 2nd paper on the intuitionistic modal logic CK and its extensions. We look at 'duality', the relationship between Kripke semantics and universal algebra. There are various dualities in the literature, but ours has some unusual features, including our 'exploding world' which satisfies all formula, including contradictions! Dualities allow results in algebra to be ported to the modal world, as we do in the 2nd half of the paper to, for example, give a description of which classes of possible worlds can be axiomatically defined. #Logic #ModalLogic
Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason

We carry out a semantic study of the constructive modal logic CK. We provide a categorical duality linking the algebraic and birelational semantics of the logic. We then use this to prove Sahlqvist style correspondence and completeness results, as well as a Goldblatt-Thomason style theorem on definability of classes of frames.

arXiv.org
RanaldCloustonAug 15, 2025
In this week's #blog I write briefly about a 2001 paper on designing lambda calculi for intuitionistic modal logic. https://blogs.fediscience.org/the-updated-scholar/2025/08/15/discussing-extended-curry-howard-correspondence-for-a-basic-constructive-modal-logic/ #logic #modalLogic #proofTheory #typeTheory
Discussing “Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic” – The Updated Scholar

ALNJun 3, 2025

New preprint: Functional Causation Beyond Spacetime: A Non-Metric Framework for Temporal Structure

Can causal direction emerge from internal asymmetries rather than geometry?

📄 PDF: https://philpapers.org/rec/LENFCB
🔍 #Causality #ModalLogic #StructuralRealism #PhilosophyOfPhysics

RanaldCloustonMay 2, 2025
My paper 'Semantical Analysis of Intuitionistic Modal Logics between CK and IK', with Jim de Groot and Ian Shillito, is now in its final edited preprint form: https://arxiv.org/abs/2408.00262 . I will travelling to #LICS #LICS2025 to present it in Singapore in late June. #logic #modalLogic
Semantical Analysis of Intuitionistic Modal Logics between CK and IK

The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also disagree on their diamond-free fragments, with only some remaining conservative over the standard axiomatisation of intuitionistic modal logic with necessity (box) alone. We show that relational Kripke semantics for CK can be extended with frame conditions for all axioms in the standard axiomatisation of IK, as well as other axioms previously studied. This allows us to answer open questions about the (non-)conservativity of such logics over intuitionistic modal logic without diamond. Our results are formalised using the Coq Proof Assistant.

arXiv.org
CubeRootOfTrueApr 25, 2025

$Trump ordered government agencies to prepare for mining the ocean floor.

Just because it is legal does not mean you should do it. Permission is not obligation.

Just say no. They have no power if you ignore them.

#JustSayNo #ModalLogic #RM3

Greg RestallApr 10, 2025

I’m in Amsterdam, about to give a talk about proof theory for modal predicate logic at the ILLC, the home base of the modal industrial complex. I have no idea how this is going to go over, but it should be a fun ride, however it turns out.

https://consequently.org/presentation/2025/mlce-illc/

#prooftheory #modalLogic

Modal Logic and Contingent Existence — consequently.org

Jesper Agdakx 🔸Apr 7, 2025
With the NWO XL consortium on Cyclic Structures in Programs and Proofs, we are looking for 6 highly motivated and talented PhD students starting in September (with some flexibility).

The topics range from Modal logic, proof theory, and coalgebras to Programming languages, concurrency, and type systems and Proof assistants (#Agda, #Rocq).

Information about the positions and application procedure can be found on the website:

cyclic-structures.gitlab.io/vacancies/

Applications will be evaluated on a rolling basis but should be submitted by the 23rd of May for full consideration.

Please forward to any strong candidates you know!

#TypeTheory #ModalLogic #Concurrency #ProgrammingLanguages #TypeSystems #ProofAssistants #CyclicStructures #PhD #Netherlands #UniversityOfGroningen #LeidenUniversity #UniversityOfTwente #TUDelft #RadboudUniversity
Vacancies

This site collects information about positions, publications and relevant news for the project “Cyclic Structures in Programs and Proofs” project, funded by NWO. The project aims to advance the theory of cyclic structures in proofs and programs, including in coalgebraic modal logic, type theory, behavioural types, and the proof assistants Agda and Rocq (formely Coq), and create a development environment for Rust based on these techniques.

Cyclic Structures in Programs and Proofs
Greg RestallJan 20, 2025

I'm glad to have space to get to writing, and the first writing project of my sabbatical has reached first-draft stage. If you're interested in modal logic, proof theory, and the metaphysics of contingent existence, have I got the paper for you!

https://consequently.org/writing/mlce-ge2/

I've got to say, I think the hypersequent calculus in this paper is pretty neat.

#ProofTheory #ModalLogic #Metaphysics

Modal Logic and Contingent Existence (Generality and Existence 2) — consequently.org

Leonardo PachecoJan 14, 2025

A short note I wrote a few months ago just got published: https://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/2293-06.pdf

I show that diamonds are already embedded in Artemov and Protopopescu's intuitionistic epistemic logic (they are just double negations).

This is part of some work I'm doing to understand diamonds in intuitionistic modal logics.

#Logic #ModalLogic