Contextual modal type theory
From MaRDI portal
Publication:5277812
DOI10.1145/1352582.1352591zbMath1367.03060OpenAlexW1990204174MaRDI QIDQ5277812
Brigitte Pientka, Aleksandar Nanevski, Frank Pfenning
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1028.3796
Modal logic (including the logic of norms) (03B45) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Logic programming (68N17)
Related Items (42)
Modalities in homotopy type theory ⋮ J-Calc: a typed lambda calculus for intuitionistic justification logic ⋮ Intuitionistic hypothetical logic of proofs ⋮ A dual-context sequent calculus for the constructive modal logic S4 ⋮ The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Modality via iterated enrichment ⋮ Inductive Beluga: Programming Proofs ⋮ A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types ⋮ Refined Environment Classifiers ⋮ Modalities Without Worlds ⋮ Unnamed Item ⋮ Unnamed Item ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ A modal type theory for formalizing trusted communications ⋮ Semantical analysis of contextual types ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ Reasoning about multi-stage programs ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Programs Using Syntax with First-Class Binders ⋮ LINCX: A Linear Logical Framework with First-Class Contexts ⋮ Higher-Order Dynamic Pattern Unification for Dependent Types and Records ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Hypothetical logic of proofs ⋮ Unnamed Item ⋮ Programming Inductive Proofs ⋮ Plugging-in proof development environments usingLocksinLF ⋮ Mechanizing proofs with logical relations – Kripke-style ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ Explicit Contexts in LF (Extended Abstract) ⋮ Case Analysis of Higher-Order Data ⋮ Unnamed Item ⋮ Harpoon: mechanizing metatheory interactively ⋮ A Logical Foundation for Environment Classifiers ⋮ Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables ⋮ Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages ⋮ Two-level Lambda-calculus ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Mechanized metatheory revisited ⋮ Processes against tests: on defining contextual equivalences ⋮ Unnamed Item ⋮ Coalgebras as Types Determined by Their Elimination Rules ⋮ Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions
Uses Software
This page was built for publication: Contextual modal type theory
