Experiments with modal types & modal logic formalizations
Literature:
- Kavvos, "Dual-Context Calculi for Modal Logic"
- Davies, Pfenning, "A Modal Analysis of Staged Computation"
- Pfenning, Davies, "A judgmental reconstruction of modal logic"
- Clouston, "Fitch-Style Modal Lambda Calculi"
- Gonzalez-Huesca, Miranda-Perea, Linares-Arevalo, "Two deductive systems for the constructive logic S4, a formal verification"
- Davies, "A Temporal-Logic Approach to Binding-Time Analysis"
- https://github.com/mietek/hilbert-gentzen/
- Murase, "Kripke-Style Contextual Modal Type Theory"