Functors are Type Refinement Systems

DOI10.1145/2676726.2676970zbMath1345.68112OpenAlexW2010912446MaRDI QIDQ2819783

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

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

Related Items (10)

Weakest preconditions in fibrations ⋮ Bifibrations of polycategories and classical linear logic ⋮ From semantics to types: the case of the imperative \(\lambda\)-calculus ⋮ The untyped computational \(\lambda \)-calculus and its intersection type discipline ⋮ A general semantic construction of dependent refinement type systems, categorically ⋮ Graded Hoare logic and its categorical semantics ⋮ An Isbell duality theorem for type refinement systems ⋮ Codensity Lifting of Monads and its Dual ⋮ Unnamed Item ⋮ Weakest preconditions in fibrations

This page was built for publication: Functors are Type Refinement Systems