Pages that link to "Item:Q4913763"
From MaRDI portal
The following pages link to Type classes for efficient exact real arithmetic in Coq (Q4913763):
Displaying 12 items.
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- On design and implementation of a generic number type for real algebraic number computations based on expression dags (Q655162) (← links)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- A formally verified proof of the central limit theorem (Q1694568) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective (Q2354911) (← links)
- ROSCoq: Robots Powered by Constructive Reals (Q2945622) (← links)
- Certified Exact Transcendental Real Number Computation in Coq (Q3543662) (← links)
- Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) (← links)
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives (Q4916067) (← links)
- Computer Certified Efficient Exact Reals in Coq (Q5200110) (← links)