Contextual modal type theory
From MaRDI portal
Recommendations
Cited in
(69)- Fibrational modal type theory
- Incorporating quotation and evaluation into Church's type theory
- Denotation of contextual modal type theory (CMTT): syntax and meta-programming
- Harpoon: mechanizing metatheory interactively
- Processes against tests: on defining contextual equivalences
- Modality via iterated enrichment
- Semantical analysis of contextual types
- Hypothetical logic of proofs
- Mechanized metatheory revisited
- A judgmental reconstruction of modal logic
- J-Calc: a typed lambda calculus for intuitionistic justification logic
- Intuitionistic hypothetical logic of proofs
- A higher-order abstract syntax approach to verified transformations on functional programs
- Explicit contexts in LF (extended abstract)
- Case analysis of higher-order data
- Functional programming with higher-order abstract syntax and explicit substitutions
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Modalities without worlds
- Programs using syntax with first-class binders
- \textsc{Lincx}: a linear logical framework with first-class contexts
- Higher-order dynamic pattern unification for dependent types and records
- Programming inductive proofs. A new approach based on contextual types
- Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
- Refined environment classifiers. Type- and scope-safe code generation with mutable cells
- Inductive beluga: programming proofs
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
- A modal type theory for formalizing trusted communications
- Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
- Mechanizing proofs with logical relations -- Kripke-style
- scientific article; zbMATH DE number 2085167 (Why is no real title available?)
- scientific article; zbMATH DE number 6174931 (Why is no real title available?)
- scientific article; zbMATH DE number 1418381 (Why is no real title available?)
- Two-level lambda-calculus
- Index-stratified types
- Internal universes in models of homotopy type theory
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
- scientific article; zbMATH DE number 7533352 (Why is no real title available?)
- POPLMark reloaded: mechanizing proofs by logical relations
- scientific article; zbMATH DE number 7204440 (Why is no real title available?)
- Dual-context calculi for modal logic
- Contextual types, explained. Invited tutorial
- Multimodal dependent type theory
- Modalities in homotopy type theory
- A case study in programming coinductive proofs: Howe's method
- Coalgebras as types determined by their elimination rules
- 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
- On the computational interpretation of \(\mathbf{CK}_{n}\) for contextual information processing
- Consistency of the theory of contexts
- A dual-context sequent calculus for the constructive modal logic S4
- A Logical Foundation for Environment Classifiers
- Contextual modal type theory with polymorphic contexts
- Partial proof terms in the study of idealized proof search
- Processes, systems \& tests: defining contextual equivalences
- A subexponential view of domains in session types
- A categorical normalization proof for the modal lambda-calculus
- A modal analysis of metaprogramming, revisited (invited talk)
- Proof search in classical propositional logic with partial proof terms
- Nominal Henkin semantics: simply-typed lambda-calculus models in nominal sets
- Multi-level contextual type theory
- Rewriting modulo in the -calculus Modulo
- A case study on logical relations using contextual types
- Gluing together proof environments: canonical extensions of LF type theories featuring locks
- Adelfa: a system for reasoning about LF specifications
- Explicit substitutions for contextual type theory
- ``Upon this quote I will build my Church thesis
- Handling mobility failures by modal types
- Semantics of pattern unification
This page was built for publication: Contextual modal type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277812)
