Modal type theory

Mike Shulman has started a discussion on modal type theory. Here are a few things in this direction – more will likely follow.

- Mike’s Mathematical Conversations talk on Synthetic Differential Cohomology on Wed. 10.24 at 6pm in the Dilworth room.
- Some notes on modal type theory here.
- nlab

Please add relevant references below. Selected references to the (very large) CS literature would be welcome.

```
The following was the proceedings of a meeting some years ago in Trieste. My paper was concerned with the modality that can be used to interprete
the calculus of constructions logic in the propositions as types logic.
Mathematical Structures in Computer Science
Volume 11, Number 4, August 2001: Modalities in Type Theory
Matt Fairtlough, Michael Mendler, Eugenio Moggi: Special issue: Modalities in type theory. 507-509
Frank Pfenning, Rowan Davies: A judgmental reconstruction of modal logic. 511-540
Peter Aczel: The Russell-Prawitz modality. 541-554
Joëlle Despeyroux, Pierre Leleu: Recursion over objects of functional type. 555-572
Jacob M. Howe: Proof search in Lax Logic. 573-588
Mauro Ferrari, Camillo Fiorentini, Pierangelo Miglioli: Extracting information from intermediate semiconstructive HA-systems - extended abstract. 589-596
```

The work on monadic semantics of computation and effect-type systems is closely related to modal type theory.

Moggi’s original work introduced the idea that different notions of computation correspond to different (strong) monads:

- Eugenio Moggi: Notions of computation and monads. Information and Computation, 93(1), 1991. (pdf)

Among the huge follow-up literature, Andrzej Filinski’s work tackles the question of how to navigate *between* different notions of computation, applying an idea he terms *monadic reflection* together with an effect type system:

- Andrzej Filinski: Representing Layered Monads. POPL 1999. (pdf)
- Andrzej Filinski: On the Relations between Monadic Semantics. TCS 375:1-3, 2007. (pdf)
- Andrzej Filinski: Monads in Action. POPL 2010. (pdf)

A more concrete illustration of these ideas is present in

- Oleg Kiselyov and Chung-chieh Shan: Embedded Probabilistic Programming. Working conference on domain-specific languages, 2009. (pdf)

where the authors describe how to use monadic reflection to embed a modality of probabilistic computations within a functional language.

Revised on April 19, 2018 at 18:36:50
by
Mike Shulman