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