GRASS unifies graded and substructural type systems by supporting arbitrary collections of grade algebras and develops categorical semantics that subsumes LNL, Adjoint Logic, and mGL.
Girard, Linear logic , Theor
7 Pith papers cite this work. Polarity classification is still indexing.
7
Pith papers citing it
citation-role summary
background 3
citation-polarity summary
roles
background 3polarities
background 3representative citing papers
Proof nets are defined for PiL with a correctness criterion, sequentialization procedure, and translation algorithm, establishing a canonical representation of sequent calculus derivations modulo rule permutations.
QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empirical robustness and formal verification than prior approaches.
The pushout of entangled and parameterized quantum information in monoidal categories yields the external tensor product on flat K-theory bundles.
Logical families of stable and total profunctors are definable by MLL+MIX proof-nets.
AI agents exploring Platonic mathematical structures via proof hypergraphs may reveal the overall architecture of formal mathematics and what makes parts of it human-accessible.
citing papers explorer
-
A unification of graded and substructural logics
GRASS unifies graded and substructural type systems by supporting arbitrary collections of grade algebras and develops categorical semantics that subsumes LNL, Adjoint Logic, and mGL.
-
Proof Nets for PiL (Full Version)
Proof nets are defined for PiL with a correctness criterion, sequentialization procedure, and translation algorithm, establishing a canonical representation of sequent calculus derivations modulo rule permutations.
-
Quantitative Linear Logic for Neuro-Symbolic Learning and Verification
QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empirical robustness and formal verification than prior approaches.
-
Entanglement of Sections: The pushout of entangled and parameterized quantum information
The pushout of entangled and parameterized quantum information in monoidal categories yields the external tensor product on flat K-theory bundles.
-
Full Definability in a Profunctorial Model
Logical families of stable and total profunctors are definable by MLL+MIX proof-nets.
-
Artificial Intelligence and the Structure of Mathematics
AI agents exploring Platonic mathematical structures via proof hypergraphs may reveal the overall architecture of formal mathematics and what makes parts of it human-accessible.
- Implementing Grassroots Logic Programs with Multiagent Transition Systems and AI (Full Version)