IMLA — PROGRAM
Days: Friday, 24 July 2026 Saturday, 25 July 2026
Friday, 24 July 2026
| 09:15-10:15 |
Controlling Computational Effects with Modalities (abstract) 60 min
1 Ben-Gurion Unversity
|
Location:
C5.09
| 10:45-11:05 |
On the Proof Theory of the Constructive µ-Calculus (abstract) 20 min
1 University of Gothenburg
|
| 11:05-11:25 |
Proof-relevant Kripke semantics of µML via fixpoints of containers (abstract) 20 min
1 University of Strathclyde
2 Coherence Research Ltd
|
Location:
C5.09
| 11:35-11:55 |
Cut-free Proof Theory for Intuitionistic PDL (abstract) 20 min
1 University of Gothenburg
2 University of Birmingham
|
| 11:55-12:15 |
The Complexity of the Constructive Master Modality (abstract) 20 min
1 Universitat de Barcelona
|
Location:
C5.09
| 13:40-14:00 |
Contextual Modal MetaML: Syntax and Full Abstraction (abstract) 20 min
1 University of Oxford
2 Nanyang Technological University
|
| 14:00-14:20 |
Towards a logical characterization of Effectful Contextual Modal Type Theory (abstract) 20 min
1 IMDEA Software Institute, Madrid
|
Location:
C5.09
| 14:30-15:30 |
Temporal resource management via graded effects and graded modal types (abstract) 60 min
1 University of Tartu
|
Location:
C5.09
| 16:00-16:20 |
A Value Trick for Modal Type Systems (abstract) 20 min
1 University of Edinburgh
|
| 16:20-16:40 |
Cover Semantics for Fitch-Style Modal Natural Deduction (abstract) 20 min
1 University of Birmingham
2 University of Edinburgh
|
| 16:40-17:00 |
Towards a labelled natural deduction for Constructive Modal Logics (abstract) 20 min
1 University College London
|
Saturday, 25 July 2026
Location:
C5.09
| 09:15-10:15 |
Semantics for Intuitionistic Modal Logics: Up From Constructive K (abstract) 60 min
1 Australian National University
|
Location:
C5.09
| 10:45-11:05 |
Higher-order Kripke models for intuitionistic and other non-classical modal logics (abstract) 20 min
1 University College London
|
| 11:05-11:25 |
Coderivative intuitionistic logics of topological and bimetric spaces (abstract) 20 min
1 National Institute of Informatics
2 Institute of Science Tokyo
|
Location:
C5.09
| 11:35-11:55 |
Polytopological Semantics for Intuitionistic Modal Logics (abstract) 20 min
1 TU Wien
2 Universitat de Barcelona
3 Institute of Science Tokyo
|
| 11:55-12:15 |
Gödel coding on fibrations and geminal categories (abstract) 20 min
1 The University of Tokyo
|
Location:
C5.09
| 13:40-14:00 |
An Unfinished Story: Decidability of IS4 (abstract) 20 min
1 University of Amsterdam, University of Southern Denmark
2 Czech Academy of Sciences
3 University of Birmingham
4 INIRIA, LIX Ecole Polytechnique
|
| 14:00-14:20 |
Second-order Intuitionistic Tense Logic (abstract) 20 min
1 University of Birmingham
|
Location:
C5.09
| 14:30-15:30 |
A Type-Theoretic Framework For Meta-programming (abstract) 60 min
1 McGill University
|
Location:
C5.09
| 16:00-16:20 |
Equality of proofs in substructural intuitionistic modal logics (abstract) 20 min
1 Tallinn University of Technology
2 Reykjavik University and Tallinn University of Technology
|
| 16:20-16:40 |
Weak constructive modal logics systematised (abstract) 20 min
1 Free University of Bozen-Bolzano
|
| 16:40-17:00 |
KE-style tableaux for a family of intuitionistic modal logics (abstract) 20 min
1 Instituto de Ciencias de la Computación, CONICET-UBA
2 Licenciatura en Ciencias de la Computación, UBA
3 Departamento de Ciencias de la Computación, UBA
|
