Semantics of Fine-Grained Mode Checking
Ariadne Suo
IRIF, Paris Cité
https://www.irif.fr/users/ariadne/index
Date(s) : 29/01/2026 iCal
11h00 - 12h30
The mode of a logic program says which parts of a predicate’s arguments are inputs, and which are outputs. A program is mode-correct when information flows consistently from outputs to inputs. We introduce a foundational calculus for mode checking based on an extension to classical linear logic, with a semantics in compact closed categories. One important application is for reasoning about intricate information flow through typecheckers. Instead of inventing ad-hoc algorithms to implement type systems, one can simply use our language to transform declarative rules directly into an algorithm, by assigning fine-grained modes to the original system.
Joint work with Neel Krishnaswami.
Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)
Catégories
