CHAD for expressive total languages
DOI10.1017/s096012952300018xarXiv2110.00446OpenAlexW3203610362MaRDI QIDQ6149934
Fernando Lucatelli Nunes, Matthijs Vákár
Publication date: 5 March 2024
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2110.00446
coalgebrasautomatic differentiationGrothendieck constructionprogramming languagesCartesian closed categoriesprogram transformationsextensive categoriesdenotational semanticsscientific computinginductive typestype systemslogical relationspolynomial functorscomma categoriesexponentiabilitylinear typesfibered categoriessoftware correctnessinitial algebra semanticsvariant typesArtin gluingcoinductive types(co)monadicitycreation of initial algebrasdependently typed languagesextensive indexed categoriesfree cocompletion under coproducts
Cites Work
- Non-canonical isomorphisms
- Least fixed point of a functor
- Introduction to extensive and distributive categories
- Categorical logic and type theory
- Pseudoalgebras and non-canonical isomorphisms
- Semantic factorization and descent
- Correctness of automatic differentiation via diffeologies and categorical gluing
- Reverse AD at higher types: pure, principled and denotationally correct
- Terminal coalgebras in well-founded set theory
- Lokal präsentierbare Kategorien. (Locally presentable categories)
- Kan extensions in enriched category theory
- Dependent Types and Fibred Computational Effects
- Introduction to Smooth Manifolds
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
- Evaluating Derivatives
- Higher-Order Containers
- Accessible Categories: The Foundations of Categorical Model Theory
- Categories for Types
- Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
- On lifting of biadjoints and lax algebras
- μ-Bicomplete Categories and Parity Games
- On the Versatility of Open Logical Relations
- Dialectica models of type theory
- Basic Category Theory
- A simple automatic derivative evaluation program
- Adjoint triangles
- Proof theory in the abstract
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
