Pages that link to "Item:Q3543662"
From MaRDI portal
The following pages link to Certified Exact Transcendental Real Number Computation in Coq (Q3543662):
Displaying 16 items.
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- Formally proving size optimality of sorting networks (Q1694569) (← links)
- Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective (Q2354911) (← links)
- A certifying square root and division elimination (Q2520687) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- Formal proofs for theoretical properties of Newton's method (Q3094171) (← links)
- A formal study of Bernstein coefficients and polynomials (Q3094174) (← links)
- Type classes for mathematics in type theory (Q3094177) (← links)
- Classical mathematics for a constructive world (Q3094179) (← links)
- Formal Verification of Exact Computations Using Newton’s Method (Q3183542) (← links)
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof (Q3453106) (← 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)
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base (Q5458427) (← links)