A certifying square root and division elimination

DOI10.1016/j.entcs.2015.10.012zbMath1351.68062OpenAlexW2183416657WikidataQ113317758 ScholiaQ113317758MaRDI QIDQ2520687

Pierre Neron

Publication date: 16 December 2016

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.10.012

zbMATH Keywords

program transformationcertifying transformationreal-number computationsemantics preservation

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Numerical algorithms for computer arithmetic, etc. (65Y04)

Uses Software

• Coq
• PVS
• OCaml

Cites Work

• Unnamed Item
• Unnamed Item
• Computing with infinite objects
• Construction of Real Algebraic Numbers in Coq
• Static Analysis of Finite Precision Computations
• Certified Exact Transcendental Real Number Computation in Coq
• A Formal Proof of Square Root and Division Elimination in Embedded Programs
• Square Root and Division Elimination in PVS

This page was built for publication: A certifying square root and division elimination