Functors are type refinement systems

DOI10.1145/2676726.2676970MaRDI QIDQ2819783zbMATH OpenOpenAlexFDO

Authors Paul-André Melliès, Noam Zeilberger

Publication date 29 September 2016

Published in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01096910/file/funts.pdf

zbMATH Keywords

category theorytype theoryrefinement types

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 4154448
• Functorial polymorphism
• Functorial ML
• An Isbell duality theorem for type refinement systems
• scientific article; zbMATH DE number 3999254

Cited in

(13)

• An Isbell duality theorem for type refinement systems
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• A fibrational tale of operational logical relations: pure, effectful and differential
• A general semantic construction of dependent refinement type systems, categorically
• Graded Hoare logic and its categorical semantics
• Weakest preconditions in fibrations
• Codensity lifting of monads and its dual
• Bifibrations of polycategories and classical linear logic
• Weakest preconditions in fibrations
• From semantics to types: the case of the imperative \(\lambda\)-calculus
• The untyped computational \(\lambda \)-calculus and its intersection type discipline
• A functorial excursion between algebraic geometry and linear logic
• From semantics to types: the case of the imperative \(\lambda\)-calculus

This page was built for publication: Functors are type refinement systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819783)