Type classes for efficient exact real arithmetic in Coq

zbMath1260.68378arXiv1106.3448MaRDI QIDQ4913763

Robbert Krebbers, Bas Spitters

Publication date: 9 April 2013

Full work available at URL: https://arxiv.org/abs/1106.3448

zbMATH Keywords

type theoryverified computationtype classesexact real arithmetic\texttt{Coq}

Mathematics Subject Classification ID

Related Items (8)

Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ ROSCoq: Robots Powered by Constructive Reals ⋮ A formally verified proof of the central limit theorem ⋮ Recycling proof patterns in Coq: case studies ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective

Uses Software

• Coq
• Matita
• C-CoRN
• Flocq
• RODES

This page was built for publication: Type classes for efficient exact real arithmetic in Coq