Translations between graded-base and linear-base graded coeffect calculi establish that both express the same context dependence while preserving types, grades, and operational semantics.
Free higher groups in homotopy type theory
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
roles
background 1polarities
background 1representative citing papers
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.
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.
Tractable relational probabilistic hyperproperties for MDPs are identified with efficient algorithms for probability-equality queries on reachability and omega-regular events, plus hardness results and a fast implementation.
Simpler delooping constructions for presented groups in HoTT using 2-polygraphs, Cayley graphs, and complexes, formalized in cubical Agda.
Presents hardness results and a sound, conditionally relatively complete verification/synthesis method for entropy objectives in MDPs via convex duality and invariant synthesis, with empirical evaluation on benchmarks.
citing papers explorer
-
Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
Translations between graded-base and linear-base graded coeffect calculi establish that both express the same context dependence while preserving types, grades, and operational semantics.