From Coinductive Proofs to Exact Real Arithmetic

DOI10.1007/978-3-642-04027-6_12zbMath1218.03035OpenAlexW2108845204MaRDI QIDQ3644745

Ulrich Berger

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

zbMATH Keywords

proof theoryprogram extractioncoinductionexact real number computation

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computation over the reals, computable analysis (03D78)

Related Items (9)

Typed vs. Untyped Realizability ⋮ Unnamed Item ⋮ Higher-order concepts for the potential infinite ⋮ Intuitionistic fixed point logic ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ Proofs, programs, processes ⋮ Program extraction in exact real arithmetic ⋮ A computer-verified monadic functional implementation of the integral ⋮ Computer Certified Efficient Exact Reals in Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: From Coinductive Proofs to Exact Real Arithmetic