Cited in
(71)- Programs using syntax with first-class binders
- Specification patterns for reasoning about recursion through the store
- Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
- Dual and axiomatic systems for constructive S4, a formally verified equivalence
- Axiomatic and dual systems for constructive necessity, a formally verified equivalence
- A note on harmony
- Intensional computation with higher-order functions
- A dual-context sequent calculus for the constructive modal logic S4
- Intuitionistic hypothetical logic of proofs
- scientific article; zbMATH DE number 7243672 (Why is no real title available?)
- Justification logic as a foundation for certifying mobile computation
- scientific article; zbMATH DE number 6287623 (Why is no real title available?)
- Fibrational modal type theory
- Subatomic natural deduction for a naturalistic first-order language with non-primitive identity
- Automatically splitting a two-stage lambda calculus
- General-elimination harmony and higher-level rules
- MetaML and multi-stage programming with explicit annotations
- Self-quotation in a typed, intensional lambda-calculus
- Incorporating quotation and evaluation into Church's type theory
- Connectionist computations of intuitionistic reasoning
- Classical natural deduction for S4 modal logic
- A general method for proving decidability of intuitionistic modal logics
- Program logics for homogeneous generative run-time meta-programming
- Nested sequents for intuitionistic modal logics via structural refinement
- Harmony in multiple-conclusion natural-deduction
- Hypothetical logic of proofs
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- Primitive recursion for higher-order abstract syntax
- SQEMA
- Crowfoot
- MetaOCaml
- BER MetaOCaml
- Flask
- Ynot
- Pesca
- VeriML
- FliPpr
- DKAL
- TAG
- cubicaltt
- Hop
- Eff
- reFLect
- HOL Light QE
- Links
- Type-specialized staged programming with process separation
- A Logical Foundation for Environment Classifiers
- Domain-free \(\lambda\mu\)-calculus
- 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
- Simply RaTT
- The Logic of Proofs as a Foundation for Certifying Mobile Computation
- Game semantics for constructive modal logic
- A proof-theoretic investigation of a logic of positions
- Propositional primal logic with disjunction
- A modal analysis of staged computation
- On the semantics of intensionality
- Modal dependent type theory and dependent right adjoints
- Strong normalization in some temporal substructural logics
- A framework for intuitionistic grammar logics
- Embedding constructive K into intuitionistic K
- Capability-based localization of distributed and heterogeneous queries
- Encoding types in ML-like languages
- Programming languages for interactive computing
- On harmony and permuting conversions
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types
- General-elimination stability
This page was built for software: MiniML
