An Isbell duality theorem for type refinement systems
DOI10.1017/S0960129517000068zbMath1390.68189arXiv1501.05115OpenAlexW2962849127MaRDI QIDQ4640309
Paul-André Melliès, Noam Zeilberger
Publication date: 17 May 2018
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1501.05115
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Categorical logic, topoi (03G30) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Algebraic (K)-theory and (L)-theory (category-theoretic aspects) (18F25)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Structural induction and coinduction in a fibrational setting
- Categorical logic and type theory
- Functors are Type Refinement Systems
- Refining Inductive Types
- Game Semantics in String Diagrams
- Forward with Hoare
- Hoare type theory, polymorphism and separation
- Logic Programming with Focusing Proofs in Linear Logic
- Adjointness in Foundations
- Normalization and the Yoneda embedding
- A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine
- Structure of categories
- An axiomatic basis for computer programming
- On closed categories of functors
- Indexed Induction and Coinduction, Fibrationally
This page was built for publication: An Isbell duality theorem for type refinement systems
