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.

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 interpretethe 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:

Among the huge follow-up literature, Andrzej Filinski's work tackles the question of how to navigate

betweendifferent notions of computation, applying an idea he termsmonadic reflectiontogether with an effect type system:A more concrete illustration of these ideas is present in

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