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
-
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.
-
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.
-
Tractable Hyperproperties for MDPs
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.
-
Delooping presented groups in homotopy type theory
Simpler delooping constructions for presented groups in HoTT using 2-polygraphs, Cayley graphs, and complexes, formalized in cubical Agda.
-
Entropy Objectives in Markov Decision Processes
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.