Semantics, specification logic, and Hoare logic of exact real computation

DOI10.46298/LMCS-20(2:17)2024MaRDI QIDQ6563064

Eike Neumann, Norbert Th. Müller, Pieter Collins, Michal Konečný, Norbert Preining, Se Won Park, Gyesik Lee, Martin Ziegler, Franz Brauße, Sunyoung Kim

Publication date: 27 June 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

decidabilityHoare logiccomputable analysisimperative programmingKleene logicreliable numericsTuring-completeness

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Quantifier elimination for the reals with a predicate for the powers of two
• The field of reals with a predicate for the powers of two
• LCF considered as a programming language
• A fundamental effect in computations on real numbers
• Feasible real random access machines
• Computation by `While' programs on topological partial algebras
• PCF extended with real numbers
• Integration in Real PCF
• Fifty years of Hoare's logic
• Topological complexity with continuous operations
• Semantics of a sequential language for exact real-number computation
• Classroom examples of robustness problems in geometric computations
• On computable numbers, with an application to the Entscheidungsproblem.
• Complexity Theory for Operators in Analysis
• Spaces allowing Type‐2 Complexity Theory revisited
• The Undecidability of Algebraic Rings and Fields
• RealLib: An efficient implementation of exact real arithmetic
• Proving Bounds on Real-Valued Functions with Computations
• Theories of Programming Languages
• Combining Coq and Gappa for Certifying Floating-Point Programs
• A Powerdomain Construction
• Soundness and Completeness of an Axiom System for Program Verification
• A Real Number Structure that is Effectively Categorical
• Complexity Theory of (Functions on) Compact Metric Spaces
• Effectivity in Spaces with Admissible Multirepresentations
• Computational complexity on computable metric spaces
• A new Characterization of Type-2 Feasibility
• A Language for Differentiable Functions
• Abstract Datatypes for Real Numbers in Type Theory
• Abstract versus concrete computation on metric partial algebras
• Why3 — Where Programs Meet Provers
• Polymorphism and separation in hoare type theory
• Some undecidable problems involving elementary functions of a real variable
• An axiomatic basis for computer programming
• Analytic Inequalities
• The Design of Core 2: A Library for Exact Numeric Computation in Geometry and Algebra
• ROUNDING-OFF ERRORS IN MATRIX PROCESSES

This page was built for publication: Semantics, specification logic, and Hoare logic of exact real computation

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