-
Notifications
You must be signed in to change notification settings - Fork 8
Home
Anton Trunov edited this page Nov 3, 2021
·
21 revisions
- A Judgmental Reconstruction of Modal Logic - Frank Pfenning, Rowan Davies (2001)
- A Modal Analysis of Staged Computation - Rowan Davies, Frank Pfenning (2001)
- A Modal Calculus for Effect Handling by Aleks Nanevski (2003)
- Contextual Modal Type Theory by Aleks Nanevski, Frank Pfenning, and Brigitte Pientka (2008)
- Denotation of contextual modal type theory (CMTT): syntax and metaprogramming by Murdoch J. Gabbay and Aleks Nanevski (2013)
- Cocon: Computation in Contextual Type Theory by Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, Rebecca Zucchini (2019)
- A Type Theory for Defining Logics and Proofs by Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rebecca Zucchini (2019)
- Semantical Analysis of Contextual Types by Brigitte Pientka, Ulrich Schöpp(2020)
- Recovering Purity with Comonads and Capabilities by Vikraman Choudhury, Neel Krishnaswami (2020)
- Dual-context calculi for modal logic by G.A. Kavvos (2020)
- Contextual Modal Types for Algebraic Effects and Handlers by Nikita Zyuzin, Aleksandar Nanevski (2021)
- Some constructive variants of S4 with the finite model property by Philippe Balbiani, Martín Diéguez, David Fernández-Duque (2021)
- A Modal Type System for Multi-Level Generating Extensions with Persistent Code by Yosihiro Yuse, Atsushi Igarashi (2006)
- Run-time Code Generation and Modal-ML by Philip Wickline, Peter Lee, Frank Pfenning (1998)
- Dual-context Modal Logic as Left Adjoint of Fitch-style Modal Logic by Kakutani, Murase, Nishiwaki (2019)
- MetaML and multi-stage programming with explicit annotations by Taha, Sheard (2000)
- Intensionality, Intensional Recursion, and the Gödel-Löb axiom by G.A. Kavvos (2020)
- Idris 2: Quantitative Type Theory in Practice - Edwin Brady (2021)
- Syntax and Semantics of Quantitative Type Theory - Robert Atkey (2018)
- Higher-Order Program Generation [phd-thesis] - Morten Rhiger (2001)
- MetaOCaml by Oleg Kiselyov.
- fpottier/metaocaml-hello-world - an attempt to demonstrate how to use MetaOCaml (4.11.1+BER) together with Dune.
- Beluga takes CMTT even further.
- Granule: graded modal types can be combined with linear types to make resource sensitivity an integral aspect of a programming language, precisely enforcing resource usage throughout the language (DP2001 is a special case of this system when the grades are removed or collapsed via the singleton semiring).
- https://github.com/AndrasKovacs/staged - Experimental staged language with dependent types