A judgmental reconstruction of modal logic
From MaRDI portal
Publication:2746757
DOI10.1017/S0960129501003322zbMath0997.03020OpenAlexW1988824860WikidataQ55933437 ScholiaQ55933437MaRDI QIDQ2746757
Publication date: 11 November 2002
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129501003322
modal logicnatural deductionintuitionistic modal logiclax logicjudgmentsMoggi's monadic metalanguage
Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Proof theory in general (including proof-theoretic semantics) (03F03) Abstract deductive systems (03B22)
Related Items (68)
Proof-theoretic semantics, a problem with negation and prospects for modality ⋮ J-Calc: a typed lambda calculus for intuitionistic justification logic ⋮ Intuitionistic hypothetical logic of proofs ⋮ Adjoint Logic with a 2-Category of Modes ⋮ A dual-context sequent calculus for the constructive modal logic S4 ⋮ On interactive proof-search for constructive modal necessity ⋮ Modalities Without Worlds ⋮ Type-safe higher-order channels with channel locality ⋮ Embedding Constructive K into Intuitionistic K ⋮ Unnamed Item ⋮ Proofs, Upside Down ⋮ On the relations between monadic semantics ⋮ SUBATOMIC INFERENCES: AN INFERENTIALIST SEMANTICS FOR ATOMICS, PREDICATES, AND NAMES ⋮ Unnamed Item ⋮ Normalization by evaluation for modal dependent type theory ⋮ A proof-theoretic universal property of determiners ⋮ A proof-theoretic semantics for exclusion ⋮ Justification logic as a foundation for certifying mobile computation ⋮ A general framework for the semantics of type theory ⋮ A modal type theory for formalizing trusted communications ⋮ UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC ⋮ Morpho-logic from a topos perspective -- application to symbolic AI ⋮ Proof-theoretic harmony: towards an intensional account ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ A note on harmony ⋮ Proofs of randomized algorithms in Coq ⋮ Dual and axiomatic systems for constructive S4, a formally verified equivalence ⋮ A framework for linear authorization logics ⋮ On the Semantics of Intensionality ⋮ Programs Using Syntax with First-Class Binders ⋮ Unnamed Item ⋮ Call-by-name Gradual Type Theory ⋮ Hoare type theory, polymorphism and separation ⋮ Bilateralism in proof-theoretic semantics ⋮ A logic inspired by natural language: quantifiers as subnectors ⋮ Maehara-style modal nested calculi ⋮ Adjoint reactive GUI programming ⋮ Brouwer's fixed-point theorem in real-cohesive homotopy type theory ⋮ Fibrational modal type theory ⋮ On harmony and permuting conversions ⋮ General-elimination stability ⋮ Classical natural deduction for S4 modal logic ⋮ Hypothetical logic of proofs ⋮ Harmony in multiple-conclusion natural-deduction ⋮ Selective Memoization with Box Types ⋮ On the unity of duality ⋮ Subatomic natural deduction for a naturalistic first-order language with non-primitive identity ⋮ Unnamed Item ⋮ Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism ⋮ The Logic of Proofs as a Foundation for Certifying Mobile Computation ⋮ A general method for proving decidability of intuitionistic modal logics ⋮ Judgmental subtyping systems with intersection types and modal types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Focused and Synthetic Nested Sequents ⋮ Unnamed Item ⋮ Proof search and certificates for evidential transactions ⋮ A Curry–Howard View of Basic Justification Logic ⋮ A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4 ⋮ Axiomatic and dual systems for constructive necessity, a formally verified equivalence ⋮ Cut-free Gentzen calculus for multimodal CK ⋮ A modal logic internalizing normal proofs ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Proof-Theoretic Semantics and Feasibility ⋮ Unnamed Item ⋮ Constructive Modalities with Provability Smack ⋮ Specifying Properties of Concurrent Computations in CLF ⋮ CATEGORICAL HARMONY AND PATH INDUCTION
This page was built for publication: A judgmental reconstruction of modal logic
