The following pages link to Contextual modal type theory (Q5277812):
Displayed 42 items.
- J-Calc: a typed lambda calculus for intuitionistic justification logic (Q276037) (← links)
- Intuitionistic hypothetical logic of proofs (Q276039) (← links)
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- A modal type theory for formalizing trusted communications (Q420842) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Harpoon: mechanizing metatheory interactively (Q2055903) (← links)
- Processes against tests: on defining contextual equivalences (Q2079681) (← links)
- Modality via iterated enrichment (Q2134835) (← links)
- Semantical analysis of contextual types (Q2200843) (← links)
- Hypothetical logic of proofs (Q2254560) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- Explicit Contexts in LF (Extended Abstract) (Q2804940) (← links)
- Case Analysis of Higher-Order Data (Q2804942) (← links)
- Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions (Q2866332) (← links)
- Modalities Without Worlds (Q2908759) (← links)
- Programs Using Syntax with First-Class Binders (Q2988654) (← links)
- LINCX: A Linear Logical Framework with First-Class Contexts (Q2988658) (← links)
- Higher-Order Dynamic Pattern Unification for Dependent Types and Records (Q3007654) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables (Q3094165) (← links)
- Refined Environment Classifiers (Q3179298) (← links)
- Inductive Beluga: Programming Proofs (Q3454100) (← links)
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages (Q3644934) (← links)
- Plugging-in proof development environments using<i>Locks</i>in<tt>LF</tt> (Q4691186) (← links)
- Mechanizing proofs with logical relations – Kripke-style (Q4691187) (← links)
- Two-level Lambda-calculus (Q4982628) (← links)
- (Q4993349) (← links)
- (Q4993352) (← links)
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types (Q5056372) (← links)
- (Q5079752) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- (Q5111317) (← links)
- (Q5155672) (← links)
- Modalities in homotopy type theory (Q5208873) (← links)
- A case study in programming coinductive proofs: Howe’s method (Q5236557) (← links)
- Coalgebras as Types Determined by Their Elimination Rules (Q5253935) (← links)
- Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
- Reasoning about multi-stage programs (Q5371979) (← links)
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (Q5372007) (← links)
- A dual-context sequent calculus for the constructive modal logic S4 (Q5889308) (← links)
- A Logical Foundation for Environment Classifiers (Q5902143) (← links)