Skip to main content
Wikispaces Classroom is now free, social, and easier than ever.
Try it today.
Pages and Files
Categorical Semantics WG
Coq for UF
Coq Working Group
Formalized Homotopy Theory
Higher Inductive Types
Homotopy Type System
how to add a plugin
IAS program participants
Informal Type Theory
Math in HoTT
Modal type theory
Notation and terminology
Add "All Pages"
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
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.
Among the huge follow-up literature, Andrzej Filinski's work tackles the question of how to navigate
different notions of computation, applying an idea he terms
together with an effect type system:
Andrzej Filinski: Representing Layered Monads. POPL 1999.
Andrzej Filinski: On the Relations between Monadic Semantics. TCS 375:1-3, 2007.
Andrzej Filinski: Monads in Action. POPL 2010.
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.
where the authors describe how to use monadic reflection to embed a modality of probabilistic computations within a functional language.
help on how to format text
Turn off "Getting Started"