The following pages link to MiniML (Q41339):
Displayed 50 items.
- Intuitionistic hypothetical logic of proofs (Q276039) (← links)
- Specification patterns for reasoning about recursion through the store (Q393092) (← links)
- Justification logic as a foundation for certifying mobile computation (Q408548) (← links)
- A note on harmony (Q452347) (← links)
- Bilateralism in proof-theoretic semantics (Q484102) (← links)
- A logic inspired by natural language: quantifiers as subnectors (Q484201) (← links)
- On harmony and permuting conversions (Q518743) (← links)
- General-elimination stability (Q526738) (← links)
- Sequent calculi and decidability for intuitionistic hybrid logic (Q764257) (← links)
- Cut-free Gentzen calculus for multimodal CK (Q764259) (← links)
- Constructive linear-time temporal logic: proof systems and Kripke semantics (Q764262) (← links)
- A proof-theoretic investigation of a logic of positions (Q1408856) (← links)
- MetaML and multi-stage programming with explicit annotations (Q1583363) (← links)
- Intensional computation with higher-order functions (Q1733061) (← links)
- Fibrational modal type theory (Q1744413) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Classical natural deduction for S4 modal logic (Q1758660) (← links)
- Encoding types in ML-like languages (Q1826630) (← links)
- Pattern matching as cut elimination (Q1882898) (← links)
- Type-specialized staged programming with process separation (Q1929349) (← links)
- Subatomic natural deduction for a naturalistic first-order language with non-primitive identity (Q2011824) (← links)
- Self-quotation in a typed, intensional lambda-calculus (Q2130593) (← links)
- Nested sequents for intuitionistic modal logics via structural refinement (Q2142093) (← links)
- Game semantics for constructive modal logic (Q2142094) (← links)
- Dual and axiomatic systems for constructive S4, a formally verified equivalence (Q2219076) (← links)
- Hypothetical logic of proofs (Q2254560) (← links)
- Harmony in multiple-conclusion natural-deduction (Q2254564) (← links)
- Connectionist computations of intuitionistic reasoning (Q2503271) (← links)
- A general method for proving decidability of intuitionistic modal logics (Q2506825) (← links)
- A framework for intuitionistic grammar logics (Q2695538) (← links)
- Domain-Free<i>λµ</i>-Calculus (Q2729625) (← links)
- Automatically Splitting a Two-Stage Lambda Calculus (Q2802484) (← links)
- Programming Languages For Interactive Computing (Q2864508) (← links)
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types (Q2974778) (← links)
- On the Semantics of Intensionality (Q2988392) (← links)
- Programs Using Syntax with First-Class Binders (Q2988654) (← links)
- Embedding Constructive K into Intuitionistic K (Q3185769) (← links)
- A modal analysis of staged computation (Q3196622) (← links)
- The Logic of Proofs as a Foundation for Certifying Mobile Computation (Q3605521) (← links)
- Capability-based localization of distributed and heterogeneous queries (Q4577810) (← links)
- Strong normalization in some temporal substructural logics (Q4914411) (← links)
- A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types (Q5056372) (← links)
- Undecidability of QLTL and QCTL with two variables and one monadic predicate letter (Q5059700) (← links)
- (Q5119390) (← links)
- Program Logics for Homogeneous Generative Run-Time Meta-Programming (Q5177336) (← links)
- General-Elimination Harmony and Higher-Level Rules (Q5213616) (← links)
- Modal dependent type theory and dependent right adjoints (Q5220184) (← links)
- Axiomatic and dual systems for constructive necessity, a formally verified equivalence (Q5231279) (← links)
- Propositional primal logic with disjunction (Q5406129) (← links)
- (Q5411470) (← links)