On the power of coercion abstraction

DOI10.1145/2103656.2103699zbMATH Open1321.68145OpenAlexW4206600381MaRDI QIDQ2942887FDOQ2942887

Authors: Julien Cretin, Didier Rémy 

Publication date: 11 September 2015

Published in: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00582570v3/file/RR-7587.pdf

Recommendations

• System F with coercion constraints
• Coercions in a polymorphic type system
• Coercive subtyping via mappings of reduction behaviour
• Soundness of Coercion in the Calculus of Constructions
• Types for Proofs and Programs

zbMATH Keywords

polymorphismsubtypingcoercionretyping functionsSystem Fconversionbounded polymorphismtype containment

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cited In (4)

• System F with coercion constraints
• Safe zero-cost coercions for Haskell
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: On the power of coercion abstraction

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