System F with coercion constraints

DOI10.1145/2603088.2603128MaRDI QIDQ4635618zbMATH OpenOpenAlexFDO

Authors Julien Cretin, Didier Rémy

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01093239/document

zbMATH Keywords

bounded polymorphismcoercionF-etafull reductionGADTspolymorphismrecursive coercionsrecursive typesretyping functionsstep-indexed semanticssubtypingSystem Ftypetype constraintstype containmenttypings

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• On the power of coercion abstraction
• Coercive subtyping for the calculus of constructions (extended abstract)
• Coercions in a polymorphic type system
• Soundness of Coercion in the Calculus of Constructions
• Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions

Cited in

(2)

• On the power of coercion abstraction
• The essence of dependent object types

This page was built for publication: System F with coercion constraints

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