Nonuniform Coercions via Unification Hints

Authors :: Enrico Tassi
Claudio Sacerdoti Coen
Claudio Sacerdoti Coen
Enrico Tassi
Source :: Electronic Proceedings in Theoretical Computer Science, Vol 53, Iss Proc. TYPES 2009, Pp 16-29 (2011), TYPES
Publication Year :: 2011
Publisher :: arXiv, 2011.
Abstract: We introduce the notion of nonuniform coercion, which is the promotion of a value of one type to an enriched value of a different type via a nonuniform procedure. Nonuniform coercions are a generalization of the (uniform) coercions known in the literature and they arise naturally when formalizing mathematics in an higher order interactive theorem prover using convenient devices like canonical structures, type classes or unification hints. We also show how nonuniform coercions can be naturally implemented at the user level in an interactive theorem prover that allows unification hints.<br />Comment: In Proceedings TYPES 2009, arXiv:1103.3111

Database :: OpenAIRE
Journal :: Electronic Proceedings in Theoretical Computer Science, Vol 53, Iss Proc. TYPES 2009, Pp 16-29 (2011), TYPES
Accession number :: edsair.doi.dedup.....a52f31c5d030ccc080065d60fb81f41f
Full Text :: https://doi.org/10.48550/arxiv.1103.3320