Containers: Constructing strictly positive types
From MaRDI portal
Recommendations
Cites work
- A predicative strong normalisation proof for a -calculus with interleaving inductive types
- Advanced Functional Programming
- Categorical logic and type theory
- Categories for Types
- Categories of containers
- Constructing polymorphic programs with quotient types
- Container types categorically
- Derivatives of containers
- Extensional constructs in intensional type theory
- Fibered categories and the foundations of naive category theory
- Generalised folds for nested datatypes
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 3989612 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 108434 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 3544242 (Why is no real title available?)
- scientific article; zbMATH DE number 3574077 (Why is no real title available?)
- scientific article; zbMATH DE number 3605078 (Why is no real title available?)
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- scientific article; zbMATH DE number 692330 (Why is no real title available?)
- Locally cartesian closed categories and type theory
- Monadic presentations of lambda terms using generalized inductive types
- Non-well-founded trees in categories
- On relating type theories and set theories
- On the interpretation of type theory in locally Cartesian closed categories
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- Representing nested inductive types using W-types
- Semantics of type theory. Correctness, completeness and independence results. With a foreword by Martin Wirsing
- The view from the left
- Two applications of analytic functors
- Types for Proofs and Programs
- Wellfounded trees in categories
Cited in
(63)- Complexity bounds for container functors and comonads
- The universal exponentiable arrow
- Generic recursive lens combinators and their calculation laws
- Deep induction: induction rules for (truly) nested types
- Universal properties of bicategories of polynomials
- Incremental computing with abstract data structures
- Continuous functions on final coalgebras
- A coalgebraic view of bar recursion and bar induction
- Modular dependent induction in Coq, Mendler-style
- Coalgebraic update lenses
- Constructive membership predicates as index types
- Comonadic notions of computation
- Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
- Proving properties about functions on lists involving element tests
- A mechanized theory of regular trees in dependent type theory
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Data types with symmetries and polynomial functors over groupoids
- Galois Connections for Recursive Types
- Higher-order containers
- A UNIVERSE OF STRICTLY POSITIVE FAMILIES
- Categories of containers
- Container types categorically
- Quotienting the delay monad by weak bisimilarity
- Polynomial functors and polynomial monads
- A syntax for higher inductive-inductive types
- Directed containers as categories
- Dependent inductive and coinductive types are fibrational dialgebras
- Multi-dimensional arrays with levels
- Partiality and Container Monads
- The costructure–cosemantics adjunction for comodels for computational effects
- Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
- Martin Hofmann's Case for Non-Strictly Positive Data Types
- Quotients, inductive types, and quotient inductive types
- Variations on inductive-recursive definitions
- Signatures and induction principles for higher inductive-inductive types
- Indexed containers
- Homotopical patch theory
- Representing nested inductive types using W-types
- A linear category of polynomial diagrams
- W-types in homotopy type theory
- Containers, monads and induction recursion
- Decomposing Comonad Morphisms.
- Protocol choice and iteration for the free cornering
- Constructing initial algebras using inflationary iteration
- Characterizing functions mappable over GADTs
- Coalgebras in functional programming and type theory
- Stabilized profunctors and stable species of structures
- Formal definitions and proofs for partial (co)recursive functions
- Inductive and coinductive predicate liftings for effectful programs
- Hefty algebras: modular elaboration of higher-order effects
- A syntax for mutual inductive families
- Formalizing two-level type theory with cofibrant exo-nat
- Comodule representations of second-order functionals
- Broad infinity and generation principles
- Data types with symmetries via action containers
- Impredicative encodings of inductive and coinductive types
- Distributive laws of monadic containers
- Terminal coalgebras and non-wellfounded sets in homotopy type theory
- Initial algebras of domains via quotient inductive-inductive types
- Formalising inductive and coinductive containers
- Program optimisations via hylomorphisms for extraction of executable code
- The list object endofunctor is polynomial
- Non-well-founded trees in categories
This page was built for publication: Containers: Constructing strictly positive types
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2566024)
