Categorical univalence of a universe does not entail function extensionality, as shown by polynomial models of type theory that refute the latter while satisfying the former.
A Fixpoint Logic and Dependent Effects for Temporal Property Verification
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
citation-role summary
background 2
citation-polarity summary
verdicts
UNVERDICTED 4roles
background 2polarities
background 2representative 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.
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.
A finitary refinement type system is sound and complete for Scott-open properties in a fixpoint-like logic over spectral Scott domains.
citing papers explorer
-
Univalence without function extensionality
Categorical univalence of a universe does not entail function extensionality, as shown by polynomial models of type theory that refute the latter while satisfying the former.
-
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.
-
Trace-Guided Synthesis of Effectful Test Generators
Underapproximate types with symbolic traces guide synthesis of test generators that outperform defaults in property-based testing and model checking for effectful programs.
-
A Complete Finitary Refinement Type System for Scott-Open Properties
A finitary refinement type system is sound and complete for Scott-open properties in a fixpoint-like logic over spectral Scott domains.