Search

• < Previous
• 1
• Next >

---

Type classes for efficient exact real arithmetic in Coq

Robbert Krebbers ; Bas Spitters.

Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. Previously, we&nbsp;[&hellip;]

---

Almost periodic functions, constructively

Bas Spitters.

The almost periodic functions form a natural example of a non-separable normed space. As such, it has been a challenge for constructive mathematicians to find a natural treatment of them. Here we present a simple proof of Bohr's fundamental theorem for almost periodic functions which we then&nbsp;[&hellip;]

---

Modalities in homotopy type theory

Egbert Rijke ; Michael Shulman ; Bas Spitters.

Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and&nbsp;[&hellip;]

---