swMATH29625MaRDI QIDQ41339FDOQ41339
Author name not available (Why is that?)
Official website: https://dl.acm.org/citation.cfm?doid=382780.382785
Cited In (70)
- Simply RaTT
- Strong normalization in some temporal substructural logics
- Capability-based localization of distributed and heterogeneous queries
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
- Specification patterns for reasoning about recursion through the store
- Dual and axiomatic systems for constructive S4, a formally verified equivalence
- Axiomatic and dual systems for constructive necessity, a formally verified equivalence
- A dual-context sequent calculus for the constructive modal logic S4
- Intensional computation with higher-order functions
- A note on harmony
- Title not available (Why is that?)
- Intuitionistic hypothetical logic of proofs
- Title not available (Why is that?)
- Justification logic as a foundation for certifying mobile computation
- Fibrational modal type theory
- Automatically splitting a two-stage lambda calculus
- Subatomic natural deduction for a naturalistic first-order language with non-primitive identity
- General-elimination harmony and higher-level rules
- MetaML and multi-stage programming with explicit annotations
- Self-quotation in a typed, intensional lambda-calculus
- Connectionist computations of intuitionistic reasoning
- Incorporating quotation and evaluation into Church's type theory
- Classical natural deduction for S4 modal logic
- Program logics for homogeneous generative run-time meta-programming
- Primitive recursion for higher-order abstract syntax
- A general method for proving decidability of intuitionistic modal logics
- Nested sequents for intuitionistic modal logics via structural refinement
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- Harmony in multiple-conclusion natural-deduction
- Hypothetical logic of proofs
- Type-specialized staged programming with process separation
- A Logical Foundation for Environment Classifiers
- Crowfoot
- MetaOCaml
- BER MetaOCaml
- Flask
- Ynot
- Pesca
- VeriML
- FliPpr
- Domain-free \(\lambda\mu\)-calculus
- DKAL
- TAG
- cubicaltt
- Hop
- Eff
- reFLect
- HOL Light QE
- Links
- Constructive linear-time temporal logic: proof systems and Kripke semantics
- Cut-free Gentzen calculus for multimodal CK
- Sequent calculi and decidability for intuitionistic hybrid logic
- Pattern matching as cut elimination
- Bilateralism in proof-theoretic semantics
- A logic inspired by natural language: quantifiers as subnectors
- The Logic of Proofs as a Foundation for Certifying Mobile Computation
- Game semantics for constructive modal logic
- Propositional primal logic with disjunction
- A proof-theoretic investigation of a logic of positions
- A modal analysis of staged computation
- Modal dependent type theory and dependent right adjoints
- On the semantics of intensionality
- A framework for intuitionistic grammar logics
- Embedding constructive K into intuitionistic K
- Encoding types in ML-like languages
- Programming languages for interactive computing
- On harmony and permuting conversions
- General-elimination stability
- Programs using syntax with first-class binders
- Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
This page was built for software: MiniML
