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.
Free higher groups in homotopy type theory
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
verdicts
UNVERDICTED 4roles
background 1polarities
background 1representative citing papers
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.
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.