# Nonuniform Coercions via Unification Hints

@inproceedings{Coen2009NonuniformCV, title={Nonuniform Coercions via Unification Hints}, author={Claudio Sacerdoti Coen and Enrico Tassi}, booktitle={TYPES}, year={2009} }

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… Expand

#### Topics from this paper

#### 10 Citations

System F with coercion constraints

- Computer Science
- CSL-LICS
- 2014

We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and… Expand

System F with Coercion Constraints Julien Cretin Didier Rémy INRIA

- 2017

We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and… Expand

A proof of Bertrand's postulate

- Mathematics, Computer Science
- J. Formaliz. Reason.
- 2012

We discuss the formalization, in the Matita Interactive Theorem Prover, of some results by Chebyshev concerning the distribution of prime numbers, subsuming, as a corollary, Bertrand's postulate. … Expand

Implementing type theory in higher order constraint logic programming

- Mathematics, Computer Science
- Mathematical Structures in Computer Science
- 2019

An extension to λProlog is proposed that allows to control the generative semantics, suspend goals over flexible terms turning them into constraints, and finally manipulate these constraints at the meta-meta level via constraint handling rules. Expand

Formalising Overlap Algebras in Matita†

- Computer Science
- Mathematical Structures in Computer Science
- 2011

Overlap Algebras are new algebraic structures designed to ease reasoning about subsets in an algebraic way within intuitionistic logic and it is found that they also ease the formalisation of formal topological results in an interactive theorem prover. Expand

Deciding Kleene Algebras in Coq

- Computer Science, Mathematics
- Log. Methods Comput. Sci.
- 2012

We present a reflexive tactic for deciding the equational theory of Kleene
algebras in the Coq proof assistant. This tactic relies on a careful
implementation of efficient finite automata algorithms,… Expand

Type classes for efficient exact real arithmetic in Coq

- Computer Science, Mathematics
- Log. Methods Comput. Sci.
- 2011

This article implements and verify the sine and cosine function, creates an additional implementation of the dense set based on Coq's fast rational numbers, and extends the hierarchy to capture order on undecidable structures, while it was limited to decidable structures before. Expand

TYPE CLASSES FOR EFFICIENT EXACT REAL ARITHMETIC IN COQ

- Computer Science
- 2013

This article implements and verify the sine and cosine function, creates an additional implementation of the dense set based on Coq's fast rational numbers, and extends the hierarchy to capture order on undecidable structures, while it was limited to decidable structures before. Expand

Theory Presentation Combinators

- Computer Science, Mathematics
- AISC/MKM/Calculemus
- 2012

The category of contexts and fibered categories are the ideal theoretical tools for this purpose and motivate and give semantics to theory presentation combinators as the foundations for a scalable library of theories. Expand

Matita Tutorial

- Computer Science
- J. Formaliz. Reason.
- 2014

Getting Started with Matita 0.0 Getting Started 94 0.1 Installing Matita 1.0 . Expand

#### References

SHOWING 1-10 OF 22 REFERENCES

Working with Mathematical Structures in Type Theory

- Computer Science
- TYPES
- 2007

This work addresses the problem of representing mathematical structures in a proof assistant which is based on a type theory with dependent types, telescopes and a computational version of Leibniz equality and proposes unification and type reconstruction heuristics that are slightly different from the ones usually implemented. Expand

Hints in Unification

- Computer Science
- TPHOLs
- 2009

All mechanisms introduced with the aim of improving the power and flexibility of the type inference algorithm for interactive theorem provers are claimed to be particular instances of a simpler and more general technique, just consisting in providing suitable hints to the unification procedure underlying type inference. Expand

A compact kernel for the calculus of inductive constructions

- Mathematics
- 2009

The paper describes the new kernel for the Calculus of Inductive Constructions (CIC) implemented inside the Matita Interactive Theorem Prover. The design of the new kernel has been completely… Expand

Packaging Mathematical Structures

- Computer Science
- TPHOLs
- 2009

This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system, and presents a key lemma for characterising the discrete logarithm, and a matrix decomposition problem. Expand

Coercive Subtyping

- Computer Science
- J. Log. Comput.
- 1999

This approach, subtyping with speciied implicit coercions is treated as a feature at the level of the logical framework; in particular, the meaning of an object being in a supertype is given by coercive deenition rules for the deenitional equality. Expand

Subset Coercions in Coq

- Computer Science
- TYPES
- 2006

A new language for writing programs with dependent types on top of the COQ proof assistant allowing to write algorithms as easily as in a practical functional programming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole COQProof apparatus. Expand

A New Look at Generalized Rewriting in Type Theory

- Computer Science
- J. Formaliz. Reason.
- 2009

This work presents a new implementation of generalized rewriting in the Coq proof assistant, making essential use of the expressive power of dependent types and the recently implemented type class mechanism. Expand

Dependently Typed Records in Type Theory

- Mathematics, Computer Science
- Formal Aspects of Computing
- 2002

The main contribution in this paper is to show that structures with dependent types and manifest fields are internally definable in a type theoretic framework extended with inductive-recursive definition, which shows that powerful modules follow from general principles without module-specific assumptions. Expand

Canonical Big Operators

- Computer Science
- TPHOLs
- 2008

It is shown how these canonical big operations played a crucial enabling role in the study of various parts of linear algebra and multi-dimensional real analysis, as illustrated by the formal proofs of the properties of determinants, of the Cayley-Hamilton theorem and of Kantorovitch's theorem. Expand

First-Class Type Classes

- Computer Science
- TPHOLs
- 2008

This work proposes an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away, and shows how it can be used to help structured programming and proving by way of examples. Expand