Constructive Modalities with Provability Smack

Abstract

I overview the work of the Tbilisi school on intuitionistic modal logics of well-founded/scattered structures and its connections with contemporary theoretical computer science. Fixed-point theorems and their consequences are of particular interest.

The paper is a modified and extended version ("Author's Cut") of my contribution for the "Leo Esakia on Duality in Modal and Intuitionistic Logics."

References in corpus (2)

• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Proceedings Workshop on Fixed Points in Computer Science

Cited by in corpus (10)

• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Dual-Context Calculi for Modal Logic
• Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion
• On the Semantics of Intensionality and Intensional Recursion
• Intensionality, Intensional Recursion, and the Gödel-Löb axiom
• Modal Logics that Bound the Circumference of Transitive Frames
• An overview of Generalised Veltman Semantics
• Proof Theory for Intuitionistic Strong Löb Logic
• The G4i analogue of a G3i calculus
• Goldblatt-Thomason Theorems for Modal Intuitionistic Logics