A dependent linear type theory is constructed by embedding linear logic into dependent type theory, yielding multiplicities that depend on variables, supporting W-types, with semantics in indexed Categories with Families and an Agda implementation.
Bounded arithmetic and propositional proof complexity
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
verdicts
UNVERDICTED 4representative citing papers
Short Resolution refutations of Ref(φ) yield satisfying assignments for φ in polynomial time via a PV1-formalizable construction, and the Proof Analysis Problem is NP-complete for Extended Frege.
A categorical duality links algebraic and birelational semantics for constructive modal logic CK, enabling Sahlqvist correspondence, completeness, and Goldblatt-Thomason definability theorems.
Completes Maksimova's classification of normal extensions of S4 by proving Craig interpolation for the six remaining open cases via Fine's frame formulas.
citing papers explorer
-
Dependent Multiplicities in Dependent Linear Type Theory
A dependent linear type theory is constructed by embedding linear logic into dependent type theory, yielding multiplicities that depend on variables, supporting W-types, with semantics in indexed Categories with Families and an Agda implementation.
-
The Proof Analysis Problem
Short Resolution refutations of Ref(φ) yield satisfying assignments for φ in polynomial time via a PV1-formalizable construction, and the Proof Analysis Problem is NP-complete for Extended Frege.
-
Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
A categorical duality links algebraic and birelational semantics for constructive modal logic CK, enabling Sahlqvist correspondence, completeness, and Goldblatt-Thomason definability theorems.
-
Interpolation above S4
Completes Maksimova's classification of normal extensions of S4 by proving Craig interpolation for the six remaining open cases via Fine's frame formulas.