From Coinductive Proofs to Exact Real Arithmetic
From MaRDI portal
Recommendations
- From coinductive proofs to exact real arithmetic: theory and applications
- Coinductive Formal Reasoning in Exact Real Arithmetic
- Logical Approaches to Computational Barriers
- Theorem Proving in Higher Order Logics
- A coinductive approach to real analysis
- A proof theory for the logic of provability in true arithmetic
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
- Coinductive field of exact real numbers and general corecursion
- Realisability for induction and coinduction with applications to constructive analysis
- Automated Deduction – CADE-20
Cites work
- scientific article; zbMATH DE number 1552509 (Why is no real title available?)
- scientific article; zbMATH DE number 2090725 (Why is no real title available?)
- scientific article; zbMATH DE number 3216998 (Why is no real title available?)
- scientific article; zbMATH DE number 2247254 (Why is no real title available?)
- scientific article; zbMATH DE number 2247255 (Why is no real title available?)
- A certified, corecursive implementation of exact real numbers
- A functional algorithm for exact real integration with invariant measures
- Affine functions and series with co-inductive real numbers
- Coinduction for exact real number computation
- Coinductive Formal Reasoning in Exact Real Arithmetic
- Constructive analysis, types and exact real numbers
- Continuous Lattices and Domains
- Continuous functions on final coalgebras
- Data structures and program transformation
- Efficient exact computation of iterated maps
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- Iteration and coiteration schemes for higher-order and nested datatypes
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Real functions incrementally computable by finite automata
- Realizability interpretation of proofs in constructive analysis
- Recursive coalgebras from comonads
- Semantics of a sequential language for exact real-number computation
Cited in
(25)- Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers
- Proofs, programs, processes
- A certified, corecursive implementation of exact real numbers
- Computable analysis and notions of continuity in \textsc{Coq}
- New Computational Paradigms
- Coinduction for exact real number computation
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
- Using theory interpretation to mechanise the reals in a theorem prover
- Program extraction in exact real arithmetic
- Certified Exact Transcendental Real Number Computation in Coq
- Productivity of Edalat-Potts exact arithmetic in constructive type theory
- Typed vs. untyped realizability
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
- Computer Certified Efficient Exact Reals in Coq
- Real Algebraic Strategies for MetiTarski Proofs
- From coinductive proofs to exact real arithmetic: theory and applications
- Affine functions and series with co-inductive real numbers
- Coinductive Formal Reasoning in Exact Real Arithmetic
- Higher-order concepts for the potential infinite
- Logical Approaches to Computational Barriers
- Realisability and adequacy for (co)induction
- A computer-verified monadic functional implementation of the integral
- Intuitionistic fixed point logic
- scientific article; zbMATH DE number 7350773 (Why is no real title available?)
- Coinductive field of exact real numbers and general corecursion
This page was built for publication: From Coinductive Proofs to Exact Real Arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3644745)
