From Coinductive Proofs to Exact Real Arithmetic

DOI10.1007/978-3-642-04027-6_12zbMath1218.03035MaRDI 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 theory; program extraction; coinduction; exact real number computation

Mathematics Subject Classification ID

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), Higher-order concepts for the potential infinite, 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