Computer Certified Efficient Exact Reals in Coq
From MaRDI portal
Publication:5200110
DOI10.1007/978-3-642-22673-1_7zbMath1260.68377arXiv1105.2751OpenAlexW3100072065MaRDI QIDQ5200110
Bas Spitters, Robbert Krebbers
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1105.2751
Related Items (4)
Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof ⋮ A Certified Reduction Strategy for Homological Image Processing ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ Formally proving size optimality of sorting networks
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A computer-verified monadic functional implementation of the integral
- A constructive theory of continuous domains suitable for implementation
- The calculus of constructions
- A compiled implementation of strong reduction
- Type classes for mathematics in type theory
- Hints in Unification
- Packaging Mathematical Structures
- Formal Verification of Exact Computations Using Newton’s Method
- Affine functions and series with co-inductive real numbers
- A monadic, functional implementation of real numbers
- Extraction in Coq: An Overview
- Certified Exact Transcendental Real Number Computation in Coq
- First-Class Type Classes
- Program Extraction from Large Proof Developments
- From Coinductive Proofs to Exact Real Arithmetic
- Comprehending monads
- How to make ad hoc proof automation less ad hoc
- Real numbers and other completions
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
- Extending Coq with Imperative Features and Its Application to SAT Verification
This page was built for publication: Computer Certified Efficient Exact Reals in Coq
