Program extraction in exact real arithmetic

DOI10.1017/S0960129513000327MaRDI QIDQ5740678zbMATH OpenOpenAlexFDO

Authors Kenji Miyamoto, Helmut Schwichtenberg

Publication date 27 July 2016

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129513000327

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Program Extraction in Constructive Analysis
• Program extraction for 2-random reals
• Practical program extraction from classical proofs
• Classical Program Extraction in the Calculus of Constructions
• Program extraction from classical proofs
• scientific article; zbMATH DE number 176743
• Computer Aided Systems Theory – EUROCAST 2005
• An operational approach to program extraction in the calculus of constructions
• Program extraction from large proof developments
• Refinement of classical proofs for program extraction

Cites work

• A certified, corecursive implementation of exact real numbers
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Computing with infinite objects
• From Coinductive Proofs to Exact Real Arithmetic
• Proofs and computations
• Proofs, programs, processes
• Realizability interpretation of proofs in constructive analysis
• Term rewriting for normalization by evaluation.
• Theory of the segment points transformation

Cited in

(18)

• Program extraction for mutable arrays
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Lookahead analysis in exact real arithmetic with logical methods
• From coinductive proofs to exact real arithmetic: theory and applications
• Minlog -- a tool for program extraction supporting algebras and coalgebras
• Program extraction from proofs: the fan theorem for uniformly coconvex bars
• Optimal Abstraction on Real-Valued Programs
• Program Extraction in Constructive Analysis
• Nonflatness and totality
• Logic for exact real arithmetic
• Limits of real numbers in the binary signed digit representation
• Normal forms, linearity, and prime algebraicity over nonflat domains
• Program extraction from nested definitions
• Constructive analysis with witnesses
• Extracting efficient exact real number computation from proofs in constructive type theory
• Proofs, programs, processes
• The world's shortest correct exact real arithmetic program?
• Verified program extraction in number theory: the fundamental theorem of arithmetic and relatives

Describes a project that uses

Uses Software

• Haskell
• Minlog

This page was built for publication: Program extraction in exact real arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740678)