# Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis

- 1 Citations
- 201 Downloads

## Abstract

This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topology and norms, in dependent type theory. This hierarchy is the backbone of a new library of formalized classical analysis, for the Coq proof assistant. It extends the Mathematical Components library, geared towards algebra, with topics in analysis. Issues of a more general nature related to the inheritance of poorer structures from richer ones arise due to this combination. We present and discuss a solution, coined forgetful inheritance, based on packed classes and unification hints.

## Keywords

Formalization of mathematics Dependent type theory Packed classes Coq## 1 Introduction

*Mathematical structures* are the backbone of the axiomatic method advocated by Bourbaki [8, 9] to spell out mathematically relevant abstractions and establish the corresponding vocabulary and notations. They are instrumental in making the mathematical literature more precise, concise, and intelligible. Modern libraries of formalized mathematics also rely on hierarchies of mathematical structures to achieve modularity, akin to interfaces in generic programming. By analogy, we call *instance* a witness of a mathematical structure on a given carrier. Mathematical structures, as interfaces, are essential to factor out the shared *vocabulary* attached to their instances. This vocabulary comes in the form of formal definitions and generic theorems, but also parsable and printable notations, and sometimes delimited automation. Some mathematical structures are *richer* than others in the sense that they extend them. Like in generic programming, rich structures *inherit* the vocabulary attached to poorer structures. Working out the precise meaning of symbols of this shared vocabulary is usually performed by enhanced type inference, which is implemented using type classes [5, 27, 28] or unification hints [3, 17, 20, 24]. In particular, these mechanisms must automatically identify inheritance relations between structures.

This paper discusses the design of a hierarchy of mathematical structures supporting a Coq [30] formal library for functional analysis, i.e., the study of spaces of functions, and of structure-preserving transformations on them. The algebraic vocabulary of linear algebra is complemented with a suitable notion of “closeness” (e.g., topology, distance, norm), so as to formalize convergence, limits, size, etc. This hierarchy is based on the *packed classes* methodology [17, 20], which represents structures using dependent records. The library strives to provide notations and theories that are as generic as they would be on paper. It is an extension of the “Mathematical Components” library [32] (hereafter MathComp), which is geared towards algebra. This extension is inspired by the Coquelicot real analysis library [7], which has its own hierarchy.

Fusing these two hierarchies, respectively from the MathComp and Coquelicot libraries, happens to trigger several interesting issues, related to inheritance relations. Indeed, when several constructions compete to infer an instance of the poorer structure, the proof assistant displays indiscernible notations, or keywords, for constructions that are actually different. This issue is not at all specific to the formalization of functional analysis: actually, the literature reports examples of this exact problem but in different contexts, e.g., in Lean’s mathlib [11, 33]. It is however more likely to happen when organizing different flavors of mathematics in a same coherent corpus, as this favors the presence of problematic competing constructions. Up to our knowledge, the problem of competing inheritance paths in hierarchies of dependent records was never discussed per se, beyond some isolated reports of failure, and of ad hoc solutions. We thus present and discuss a general methodology to overcome this issue, coined *forgetful inheritance*, based on packed classes and unification hints.

The paper is organized as follows: in Sect. 2, we recall the packed classes methodology, using a running example. Section 3 provides two concrete examples of the typical issues raised by the presence of competing inheritance paths, before describing the general issue, drawing its solution, and comparing with other type-class-like mechanisms. Finally, Sect. 4 describes the design of our hierarchy of structures for functional analysis, and its features, before Sect. 5 concludes.

## 2 Structures, Inheritance, Packed Classes

We recall some background on the representation of mathematical structures in dependent type theory, and on the construction of hierarchies using packed classes. For that purpose, we use a toy running example (see the accompanying file Open image in new window [1]), loosely based on the case study presented in Sect. 4.

### 2.1 Dependent Records

In essence, a mathematical structure attaches to a carrier set some data (e.g., operators of the structure, collections of subsets of the carrier) and prescribed properties about these data, called the *axioms* of the structure. The Calculus of Inductive Constructions [16], as implemented, e.g., by Coq [30], Agda [29], or Lean [21, 22], provides a *dependent record* construct, which allows to represent a given mathematical structure as a type, and its instances as terms of that type. A dependent record is an inductive type with a single constructor, which generalizes dependent pairs to dependent tuples. The elements of such a tuple are the arguments of the single constructor. They form a *telescope* [10], i.e., collection of terms, whose types can depend on the previous items in the tuple.

### 2.2 Inference of Mathematical Structures

*Packed classes*[17, 20] provide a robust and systematic approach to the organization of structures into hierarchies. In this approach, a

*structure*is a two-field record, which associates a carrier with a

*class*. A class encodes the inheritance relations of the structure and packages various

*mixins*. Mixins in turn provide the data, and their properties. In Coq, Open image in new window and Open image in new window are synonyms, but we reserve the latter for record types that represent actual structures. Let us explain the basics of inference of mathematical structures with packed classes by replacing the structure of Sect. 2.1 with two structures represented as packed classes. The first one provides just a binary operator: Since the Open image in new window structure is expected to be the bottom of the hierarchy, we are in the special class where the class is the same as the mixin (here, the class would be

*equal*to Open image in new window ). To endow the operator Open image in new window with a generic infix notation, we introduce a definition Open image in new window , parameterized by an instance of Open image in new window . In the definition of the corresponding notation, the wildcard Open image in new window is a placeholder for the instance of Open image in new window to be inferred from the context. We can build an instance of the Open image in new window structure with the type of integers as the carrier and the subtraction of integers for the operator: But defining an instance is not enough to make the Open image in new window notation available: To type-check the expression just above, Coq needs to fill the wildcard in the Open image in new window notation, which amounts to solving the equation Open image in new window , where Open image in new window is the definitional equality (i.e., equality up to the conversion rules of Coq type theory [30, Section “Conversion Rules” in Chapter “Calculus of Constructions”]). One can indicate that the instance Open image in new window is a

*canonical*solution by declaring it as a

*canonical instance*: This way, Coq fills the wildcard in Open image in new window with Open image in new window and retrieves as expected the subtraction for integers.

### 2.3 Inheritance and Packed Classes

^{1}at line 7. It is the class that defines the inheritance relation between Open image in new window and Open image in new window (at line 6 precisely). The definitions above are however not enough to achieve proper inheritance. For example, Open image in new window does not yet enjoy the Open image in new window notation coming with the Open image in new window structure: Here, Coq tries to solve the following equation

^{2}: The solution consists in declaring a canonical way to build a Open image in new window structure out of a Open image in new window structure in the form of a function that Coq can use to solve the equation above (using Open image in new window in this particular case):

## 3 Inheritance with Packed Classes and type classes

When several inheritance paths compete to establish that one structure extend the other, the proof assistant may display misleading information to the user and prevent proofs.

### 3.1 Competing Inheritance Paths

We extend the running example of Sect. 2 with a third and last structure. Our objective is to implement a toy generalisation of the mathematical notion of pseudometric space. This is done by introducing a reflexive relation mimicking the belonging of one of the argument to a unit ball around the other argument. The Open image in new window structure below provides a binary relation (line 2) together with a property of reflexivity (line 3):

*does not*commute definitionally.

This is of course not specific to Cartesian products and similar problems would also occur when lifting dependent products, free algebras, closure, completions, etc., on metric spaces, topological groups, etc. as well as in simpler settings without generic constructions as illustrated by our last example.

As a consequence of the definition of Open image in new window , the following lemma about balls is always true for any Open image in new window :

Since the generic lemma Open image in new window holds, the user might expect to use it to prove a version specialized to integers. This is however not the case as the following script shows:

The solution to the problems explained in this section is to ensure definitional equality by including poorer structures into richer ones; this way, “deducing” one structure from the other always amounts to erasure of data, and this guarantees there is a unique and canonical way of getting it. We call this technique *forgetful inheritance*, as it is reminiscent of forgetful functors in category theory.

### 3.2 Forgetful Inheritance with Packed Classes

*definitionally*. Indeed, the only way to achieve commutation is to have Open image in new window be a mere erasure. This means that one needs to include inside each instance of Open image in new window a canonical Open image in new window (line 7 below). Furthermore the Open image in new window must record the compatibility between the operators Open image in new window and Open image in new window (line 4 below): Since every Open image in new window includes a canonical Open image in new window , the construction of the canonical Open image in new window given a Open image in new window is exactly a projection: As a consequence, the equation holds with Open image in new window and the diagram in Fig. 1 (properly updated with the new Open image in new window structure) commutes definitionally, and so does the diagram in Fig. 2, for the same reasons.

*Factories.* Because of the compatibility axioms required by forgetful inheritance, the formal definition of a structure can depart from the expected presentation. In fact, with forgetful inheritance, the very definition of a mathematical structure should be read in *factories*, i.e., functions that construct the mixins starting from only the expected axioms. And
Open image in new window
records are rather interfaces, in a software engineering terminology. Note that just like there can be several equivalent presentations of a same mathematical stuctures, several mixins can be associated with a same target
Open image in new window
.

The second part of this paper provides concrete examples of factories for our hierarchy for functional analysis.

### 3.3 Forgetful Inheritance with type classes

Type class mechanisms [5, 27, 28] propose an alternative implementation of hierarchies. Inference relations are coded using parameters rather than projections, and proof search happens by enhancing the resolution of implicit arguments. But the issue of competing inheritance paths does not pertain to the inference mechanism at stake, nor to the prover which implements them. Its essence rather lies in the non definitionally commutative diagrams as in Fig. 1 and Fig. 2.

We illustrate this with a type classes version of our examples, in both Coq and Lean, using a semi-bundled approach (see the accompanying files
Open image in new window
and
Open image in new window
[1]). Compared to the packed class approach, hierarchies implemented using type classes remove the *structure* layer, which packages the carrier and the *class*. Hence our example keeps only the records whose name starts with is, declares them as type classes, and substitutes
Open image in new window
declarations with appropriate
Open image in new window
declarations.

Because it triggers no “backtracking search”, the use of packed classes and unification hints described in this paper avoids some issues encountered in mathlib [33, Sect. 4.3], which are more explicitly detailed in the report on the implementation of type classes in Lean 4 [26]. We do not know either how a type class version of forgetful inheritance would interact with the performance issues described in the latter paper, or whether tabling helps. Moreover, with the current implementations of type classes in both Coq and Lean, different choices on bundling may have dramatic consequences on resolution feasibility and performance. For example, former experiments in rewriting MathComp with type classes in Coq did not scale up to modules on a ring. Incidentally, our companion file Open image in new window illustrates some predictability issues of the current implementation of Coq type classes.

## 4 The Mathematical Components Analysis Library

The Coquelicot library comes with its own hierarchy of mathematical structures and the intent of the MathComp-Analysis library is to improve it with the algebraic constructs of the MathComp library, for the analysis of multivariate functions for example. This section explains three applications of forgetful inheritance that solve three design issues of a different nature raised by merging MathComp and Coquelicot, as highlighted in Fig. 3.

*topological space*is a set endowed with a topology, i.e., a total collection of open sets closed under finite intersection and arbitrary unions. Equivalently, a topology can be described by the

*neighborhood filter*of each point. A

*neighborhood*of a point

*x*is a set containing an open set around

*x*; the neighborhood filter of a point

*x*is the set of all neighborhoods of

*x*. In MathComp-Analysis, neighborhood filters are the primary component of topological spaces.

*Pseudometric spaces*are intermediate between topological and metric spaces. They were introduced as the minimal setting to handle Cauchy sequences. In Coquelicot, pseudometric spaces are called “uniform spaces” and are formalized as spaces endowed with a suitable Open image in new window predicate. This is the topic of Sect. 4.1. Coquelicot also provides

*normed spaces*, i.e., \(\mathbb {K}\)-vector spaces

*E*endowed with a suitable norm. On the other hand, in MathComp, the minimal structure with a norm operator corresponds to

*numerical domains*[12, Chap. 4][13, Sect. 3.1], i.e., integral domains with order and absolute value. This situation led to a generalization of MathComp described in Sect. 4.2. Finally, in Sect. 4.3, we explain how to do forgetful inheritance across the two distinct libraries MathComp and MathComp-Analysis.

### 4.1 Forgetful Inheritance from Pseudometric to Topological Spaces

When formalizing topology, we run into a problem akin to Sect. 3.1 because we face several competing notions of neighborhoods; we solve this issue with forgetful inheritance as explained in Sect. 3.

*p*can be defined at the level of topological spaces using the notion of open as a set

*A*that contains an open set containing

*p*:

*A*that contains a ball containing

*p*:

Here, our definition of topological space departs from the standard definition as a space endowed with a family of subsets containing the full set and the empty set and closed under union and by finite intersection. However, the latter definition can be recovered from the former. Factories (see Sect. 3.2) are provided for users who want to give only Open image in new window and to infer Open image in new window (using [31, file topology.v, definition topologyOfOpenMixin]), or the other way around.

### 4.2 Forgetful Inheritance from Numerical Domain to Normed Abelian Group

The second problem we faced when developing the MathComp-Analysis library is the competing formal definitions of norms and absolute values. The setting is more complicated than Sect. 4.1 as it involves amending the hierarchy of mathematical structures of the MathComp library.

While the codomain of a norm is always the set of (non-negative) reals, an absolute value on a Open image in new window is always an endofunction Open image in new window of type Open image in new window . Thanks to this design choice, the absolute value preserves some information about its input, e.g., the integrality of an integer. On the other hand, the Coquelicot library also had several notions of norms: the absolute value of the real numbers (from the Coq standard library), the absolute value of a structure for rings equipped with an absolute value, and the norm operator of normed modules (the latter two are Coquelicot-specific).

We hence generalize the norm provided by the MathComp library to encompass both absolute values on numerical domains and norms on vector spaces, and share notation and lemmas. This is done by introducing a new structure in MathComp called Open image in new window , for normed Abelian groups, since Abelian groups are called \(\mathbb {Z}\)-modules in MathComp. This structure is now the poorest structure with a norm, which every subsequent normed type will inherit from.

The definition of the Open image in new window structure requires to solve a mutual dependency problem. Indeed, to state the fundamental properties of norms, such as the triangle inequality, the codomain of the norm function should be at least an ordered and normed Abelian group, requiring Open image in new window to be parameterized by such a structure. However the codomain should also inherit from Open image in new window to share the notations for norm and absolute value.

*without*declaring inheritance from Open image in new window (yet to be defined). More precisely, the class of Open image in new window includes the mixin for Open image in new window (at line 5 below), which will allow for forgetful inheritance: Finally, we define the class of Open image in new window , parameterized by a Open image in new window : It is only then that we declare inheritance from the Open image in new window structure to Open image in new window , effectively implementing forgetful inheritance. We finally end up with a norm of the general type

*Illustration: sharing of norm notation and lemmas.*As an example, we explain the construction of two norms and show how they share notation and lemmas. In MathComp, the type of matrices is Open image in new window where Open image in new window is the type of coefficients. The norm Open image in new window takes the maximum of the absolute values of the coefficients: This definition uses the generic big operator [6] to define a “big max” operation out of the binary operation Open image in new window . Similarly, we define a norm for pairs of elements by taking the maximum of the absolute value of the two projections

^{3}: We then go on proving that these definitions satisfy the properties of the norm and declare canonical instances of Open image in new window for matrices and pairs (see [31] for details). All this setting is of course carried out in advance and the user only sees one notation and one set of lemmas (for example Open image in new window for the triangle inequality), so that (s)he can mix various norms transparently in the same development, as in the following two examples:

One could fear that the newly introduced structures make the library harder to use since that, to declare a canonical Open image in new window instance, a user also needs now to declare canonical Open image in new window and Open image in new window instances of the same type. Here, the idea of factories (Sect. 3.2) comes in handy for the original Open image in new window mixin has been re-designed as a factory producing Open image in new window , Open image in new window , and Open image in new window mixins in order to facilitate their declaration.

### 4.3 Forgetful Inheritance from Normed Modules to Pseudometric Spaces

The combination of the MathComp library with topological structures ultimately materializes as a mathematical structure for *normed modules*. It is made possible by introducing an intermediate structure that combines norm (from algebra) with pseudometric (from topology) into normed Abelian groups. The precise justification for this first step is as follows.

Since normed Abelian groups have topological and pseudometric space structures induced by the norm, Open image in new window should inherit from Open image in new window . To do so, we can (1) insert a new structure above Open image in new window , or (2) create a common extension of Open image in new window and Open image in new window . We choose (2) to avoid amending the MathComp library. This makes both Open image in new window and its extension Open image in new window normed Abelian groups, where the former is inadequate for topological purposes.

We ensured that the structure of normed modules indeed serves its intended purpose of enabling multivariate functional analysis by generalizing existing theories of Bachmann-Landau notations and of differentiation [2, Sect. 4].

## 5 Conclusion and Related Work

This paper has two main contributions: forgetful inheritance using packed classes, and the hierarchy of the MathComp-Analysis library. The latter library is still in its infancy and covers far less real and complex analysis than the libraries available in HOL Light and Isabelle/HOL [19, 23]. However, differences in foundations matter here, and the use of dependent types in type-class-like mechanisms is instrumental in the genericity of notations illustrated in this paper. Up to our knowledge, no other existing formal library in analysis has comparable sharing features.

The methodology presented in this paper to tame competing inheritance paths in hierarchies of dependent records is actually not new. The original description of packed classes [17, end of Sect. 3.1] already mentions that a choice operator (in fact, a mixin) should be included in the definition of a structure for countable types, even if choice operators can be defined for countable types in Coq without axiom. Yet, although the MathComp library uses forgetful inheritance at several places in its hierarchy, this solution was never described in earlier publications, nor was the issue precisely described. Proper descriptions, as well as the comparison with other inference techniques, are contributions of the present paper.

As explained in Sect. 3.3, type classes based on augmented inference of implicit arguments also allow for a variant of forgetful inheritance. For instance, Buzzard et al. mention that this pattern is used for defining metric spaces both in Lean and Isabelle/HOL’s libraries [11, Sect. 3]. In the same paper, the authors describe another formalization issue, about completing abelian groups and rings, pertaining to the same problem [11, Sect. 5.3], and which can be solved as well using forgetful inheritance.

Extensional flavors of dependent type theory could make the problematic diagram in Fig. 1 commute judgmentally. However, to the best of our knowledge, the related tools [4, 15] available at the time of writing do not implement any of the type class mechanisms discussed here.

Packed classes, and forgetful inheritance, already proved robust and efficient enough to formalize and populate large hierarchies [18], where “large” applies both to the number of structures and to the number of instances. Arguably, this approach also has drawbacks: defining deep hierarchies becomes quite verbose, and inserting new structures is tedious and error-prone. We argue that, compared to their obvious benefits in control and efficiency of the proof search, this is not a fundamental issue. As packed classes are governed by systematic patterns and invariants, this rather calls for more inspection [25] and automated generation [14] tooling, which is work in progress.

## Footnotes

- 1.
The notation :> in the structure declares the carrier as a

*coercion*[30, Chapter “Implicit Coercions”], which means that Coq has the possibility to use the function Open image in new window to fix type-mismatches, transparently for the user. - 2.
The application of Open image in new window is not necessary in our case thanks to the coercion explained in footnote (see footnote 1).

- 3.
The actual code of Open image in new window and Open image in new window is slightly more complicated because it uses a type for non-negative numeric values, see [31, file normedtype.v].

## Notes

### Acknowledgments

The authors are grateful to Georges Gonthier for the many fruitful discussions that helped rewriting parts of MathComp and MathComp-Analysis library. We also thank Arthur Charguéraud and all the anonymous reviewers for their comments on the successive versions of this paper.

## References

- 1.Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Formalizing functional analysis structures in dependent type theory (accompanying material). https://math-comp.github.io/competing-inheritance-paths-in-dependent-type-theory (2020), contains the files packed_classes.v, packed_classes.v, type_classes.lean, and scalar_notations.v, and a stand-alone archive containing snapshots of the Mathematical Components [32] and Analysis [31] libraries
- 2.Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason.
**11**, 43–76 (2018)MathSciNetzbMATHGoogle Scholar - 3.Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 84–98. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_8CrossRefzbMATHGoogle Scholar
- 4.Bauer, A., Gilbert, G., Haselwarter, P.G., Pretnar, M., Stone, C.A.: Design and implementation of the andromeda proof assistant. CoRR abs/1802.06217 (2018). http://arxiv.org/abs/1802.06217
- 5.Bauer, A., Gross, J., Lumsdaine, P.L., Shulman, M., Sozeau, M., Spitters, B.: The HoTT library: a formalization of homotopy type theory in Coq. In: 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), Paris, France, 16–17 January 2017, pp. 164–172. ACM (2017)Google Scholar
- 6.Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86–101. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_11CrossRefGoogle Scholar
- 7.Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci.
**9**(1), 41–62 (2015)MathSciNetCrossRefGoogle Scholar - 8.Bourbaki, N.: The architecture of mathematics. Am. Math. Mon.
**57**(4), 221–232 (1950), http://www.jstor.org/stable/2305937 - 9.Bourbaki, N.: Théorie des ensembles. Éléments de mathématique. Springer (2006). Original Edition published by Hermann, Paris (1970)Google Scholar
- 10.de Bruijn, N.G.: Telescopic mappings in typed lambda calculus. Inf. Comput.
**91**(2), 189–204 (1991)MathSciNetCrossRefGoogle Scholar - 11.Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New Orleans, LA, USA, 20–21 January 2020, pp. 299–312. ACM (2020)Google Scholar
- 12.Cohen, C.: Formalized algebraic numbers: construction and first-order theory. (Formalisation des nombres algébriques : construction et théorie du premier ordre). Ph.D. thesis, Ecole Polytechnique X (2012). https://pastel.archives-ouvertes.fr/pastel-00780446
- 13.Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logic. Methods Comput. Sci.
**8**(1) (2012). https://doi.org/10.2168/LMCS-8(1:2)2012 - 14.Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi (2020). Accepted in the proceedings of FSCD 2020. https://hal.inria.fr/hal-02478907
- 15.Constable, R.L., et al.: Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Upper Saddle River (1986)Google Scholar
- 16.Coquand, T., Paulin, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52335-9_47CrossRefGoogle Scholar
- 17.Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_23CrossRefGoogle Scholar
- 18.Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_14
- 19.Harrison, J.: The HOL Light System REFERENCE (2017). https://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
- 20.Mahboubi, A., Tassi, E.: Canonical structures for the working Coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 19–34. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_5CrossRefGoogle Scholar
- 21.Microsoft Reasearch: L\(\exists \forall \)N THEOREM PROVER (2020). https://leanprover.github.io
- 22.de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (System Description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26CrossRefGoogle Scholar
- 23.Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle HOL: A Proof Assistant for Higher-Order Logic. Springer (2019). https://isabelle.in.tum.de/doc/tutorial.pdf
- 24.Saïbi, A.: Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types. Application à la Théorie des Catégories. (Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory). Ph.D. thesis, Pierre and Marie Curie University, Paris, France (1999)Google Scholar
- 25.Sakaguchi, K.: Validating mathematical structures. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNAI, vol. 12167, pp. 138–157. Springer, Heidelberg (2020)Google Scholar
- 26.Selsam, D., Ullrich, S., de Moura, L.: Tabled typeclass resolution (2020). https://arxiv.org/abs/2001.04301
- 27.Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_23CrossRefGoogle Scholar
- 28.Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci.
**21**(4), 795–825 (2011)MathSciNetCrossRefGoogle Scholar - 29.The Agda Team: The Agda User Manual (2020). https://agda.readthedocs.io/en/v2.6.0.1. Version 2.6.0.1
- 30.The Coq Development Team: The Coq Proof Assistant Reference Manual. Inria (2019). https://coq.inria.fr. Version 8.10.2
- 31.The Mathematical Components Analysis Team: The Mathematical Components Analysis library (2017). https://github.com/math-comp/analysis
- 32.The Mathematical Components Team: The Mathematical Components library (2007). https://github.com/math-comp/math-comp
- 33.The mathlib Community: The lean mathematical library. In: 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New Orleans, LA, USA, 20–21 January 2020, pp. 367–381. ACM (2020)Google Scholar