Pages that link to "Item:Q2746757"
From MaRDI portal
The following pages link to A judgmental reconstruction of modal logic (Q2746757):
Displaying 50 items.
- Proof-theoretic semantics, a problem with negation and prospects for modality (Q266652) (← links)
- J-Calc: a typed lambda calculus for intuitionistic justification logic (Q276037) (← links)
- Intuitionistic hypothetical logic of proofs (Q276039) (← links)
- Justification logic as a foundation for certifying mobile computation (Q408548) (← links)
- A modal type theory for formalizing trusted communications (Q420842) (← links)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← 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)
- Cut-free Gentzen calculus for multimodal CK (Q764259) (← links)
- A modal logic internalizing normal proofs (Q764264) (← links)
- On the relations between monadic semantics (Q879354) (← links)
- A proof-theoretic universal property of determiners (Q893600) (← links)
- Proofs of randomized algorithms in Coq (Q923886) (← links)
- A proof-theoretic semantics for exclusion (Q1689564) (← links)
- Maehara-style modal nested calculi (Q1734264) (← links)
- Fibrational modal type theory (Q1744413) (← links)
- Classical natural deduction for S4 modal logic (Q1758660) (← links)
- Subatomic natural deduction for a naturalistic first-order language with non-primitive identity (Q2011824) (← links)
- Proof search and certificates for evidential transactions (Q2055859) (← links)
- On interactive proof-search for constructive modal necessity (Q2133450) (← links)
- Dual and axiomatic systems for constructive S4, a formally verified equivalence (Q2219076) (← links)
- Adjoint reactive GUI programming (Q2233414) (← links)
- Hypothetical logic of proofs (Q2254560) (← links)
- Harmony in multiple-conclusion natural-deduction (Q2254564) (← links)
- A framework for linear authorization logics (Q2449046) (← links)
- On the unity of duality (Q2482843) (← links)
- A general method for proving decidability of intuitionistic modal logics (Q2506825) (← links)
- Judgmental subtyping systems with intersection types and modal types (Q2510384) (← links)
- Proof-theoretic harmony: towards an intensional account (Q2695033) (← links)
- Focused and Synthetic Nested Sequents (Q2811354) (← links)
- A Curry–Howard View of Basic Justification Logic (Q2820702) (← links)
- Specifying Properties of Concurrent Computations in CLF (Q2871839) (← links)
- Modalities Without Worlds (Q2908759) (← links)
- Proofs, Upside Down (Q2937799) (← 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)
- Hoare type theory, polymorphism and separation (Q3546051) (← links)
- The Logic of Proofs as a Foundation for Certifying Mobile Computation (Q3605521) (← links)
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory (Q4640312) (← links)
- (Q4993352) (← links)
- Call-by-name Gradual Type Theory (Q4993354) (← links)
- (Q5028422) (← links)
- (Q5079752) (← links)
- A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4 (Q5089022) (← links)
- (Q5111322) (← links)
- (Q5111325) (← links)
