From Coinductive Proofs to Exact Real Arithmetic
From MaRDI portal
Publication:3644745
DOI10.1007/978-3-642-04027-6_12zbMath1218.03035MaRDI QIDQ3644745
Publication date: 12 November 2009
Published in: Computer Science Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-04027-6_12
03F60: Constructive and recursive analysis
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03D78: Computation over the reals, computable analysis
Related Items
Unnamed Item, Computer Certified Efficient Exact Reals in Coq, Program extraction in exact real arithmetic, Proofs, programs, processes, A computer-verified monadic functional implementation of the integral, Intuitionistic fixed point logic, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), Typed vs. Untyped Realizability
Cites Work
- Data structures and program transformation
- A certified, corecursive implementation of exact real numbers
- Coinduction for exact real number computation
- Realizability interpretation of proofs in constructive analysis
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- Iteration and coiteration schemes for higher-order and nested datatypes
- Efficient exact computation of iterated maps
- Real functions incrementally computable by finite automata
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Semantics of a sequential language for exact real-number computation
- Recursive coalgebras from comonads
- Constructive analysis, types and exact real numbers
- Affine functions and series with co-inductive real numbers
- Coinductive Formal Reasoning in Exact Real Arithmetic
- Continuous Lattices and Domains
- A Functional Algorithm for Exact Real Integration with Invariant Measures
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
