Nonuniform Coercions via Unification Hints
Claudio Sacerdoti Coen (University of bologna), Enrico Tassi, (Microsoft Research - INRIA Joint Centre)
TL;DR
This paper introduces nonuniform coercions, a flexible method for type promotion in theorem proving, generalizing uniform coercions and leveraging unification hints for practical implementation.
Contribution
It formalizes nonuniform coercions, demonstrating their natural fit in higher-order theorem provers and providing a way to implement them using unification hints.
Findings
Nonuniform coercions generalize uniform coercions.
They can be implemented using unification hints.
Enhance flexibility in formalizing mathematics.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.