Imagen de Portada

An Imperative Language for Verified Exact Real-Number Computation

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Bauer, Andrej, Park, Sewon, Simpson, Alex
Formato:	Preprint
Publicado:	2024
Materias:	Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Formalizing Hyperspaces and Operations on Subsets of Polish spaces over Abstract Exact Real Numbers
por: Konečný, Michal, et al.
Publicado: (2024)

Comodule Representations of Second-Order Functionals
por: Ahman, Danel, et al.
Publicado: (2024)

Extracting efficient exact real number computation from proofs in constructive type theory
por: Konečný, Michal, et al.
Publicado: (2022)

Equivalence and Conditional Independence in Atomic Sheaf Logic
por: Simpson, Alex
Publicado: (2024)

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
por: de Medeiros, Markus, et al.
Publicado: (2026)

On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number
por: Gallego-Hernández, Jorge, et al.
Publicado: (2025)

Towards Verifying Exact Conditions for Implementations of Density Functional Approximations
por: Helal, Sameerah, et al.
Publicado: (2024)

Sheaves as oracle computations
por: Ahman, Danel, et al.
Publicado: (2026)

A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs
por: Bortin, Maksym
Publicado: (2020)

Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)
por: Dudenhefner, Andrej
Publicado: (2022)

Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
por: Dudenhefner, Andrej
Publicado: (2026)

Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics
por: Ambridge, Todd Waugh
Publicado: (2024)

Pleasant Imperative Program Proofs with GallinaC
por: Fort, Frédéric, et al.
Publicado: (2025)

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
por: Brough, Jackson
Publicado: (2026)

Verification of Linear Dynamical Systems via O-Minimality of the Real Numbers
por: Karimov, Toghrul
Publicado: (2024)

MCAC: A Model Counting Algorithm for Exact Computation of Error Metrics of Approximate Circuits
por: Ramprasath, S, et al.
Publicado: (2024)

Verifying Peephole Rewriting In SSA Compiler IRs
por: Bhat, Siddharth, et al.
Publicado: (2024)

Verified SHAP: Provable Bounds for Exact Shapley Values of Neural Networks
por: Boetius, David, et al.
Publicado: (2026)

Verifying Numerical Methods with Isabelle/HOL
por: Bryant, Dustin, et al.
Publicado: (2025)

A Survey of Interactive Verifiable Computing: Utilizing Low-degree Polynomials
por: Wang, Angold
Publicado: (2025)

Satisfiability Modulo Theories for Verifying MILP Certificates
por: Wood, Kenan, et al.
Publicado: (2023)

Wait-Only Broadcast Protocols are Easier to Verify
por: Guillou, Lucie, et al.
Publicado: (2025)

Verified and Optimized Implementation of Orthologic Proof Search
por: Guilloud, Simon, et al.
Publicado: (2025)

Bridging Computational Notions of Depth
por: Bienvenu, Laurent, et al.
Publicado: (2024)

On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue
por: Bauer, Esaïe, et al.
Publicado: (2025)

A uniform cut-elimination theorem for linear logics with fixed points and super exponentials
por: Bauer, Esaïe, et al.
Publicado: (2025)

Verifying SQL Queries using Theories of Tables and Relations
por: Mohamed, Mudathir, et al.
Publicado: (2024)

Dynamic Probability Logic: Decidability & Computability
por: Chopoghloo, Somayeh, et al.
Publicado: (2024)

Fixed Point Theorems in Computability Theory
por: Terwijn, Sebastiaan A.
Publicado: (2024)

Computing with Infinite Objects: the Gray Code Case
por: Spreen, Dieter, et al.
Publicado: (2021)

Verifying Global Two-Safety Properties in Neural Networks with Confidence
por: Athavale, Anagha, et al.
Publicado: (2024)

VerifyThis 2019: A Program Verification Competition (Extended Report)
por: Dross, Claire, et al.
Publicado: (2020)

Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic (Long Version)
por: Barenbaum, Pablo
Publicado: (2026)

Formally Verified Animation for RoboChart using Interaction Trees
por: Ye, Kangfeng, et al.
Publicado: (2023)

Exact Exploration
por: Blass, Andreas, et al.
Publicado: (2024)

Queries With Exact Truth Values in Paraconsistent Description Logics
por: Bienvenu, Meghyn, et al.
Publicado: (2024)

Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics
por: Losavio, Lidia, et al.
Publicado: (2025)

Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
por: Komel, Anja Petković, et al.
Publicado: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
por: Coglio, Alessandro, et al.
Publicado: (2025)

Measuring Decidability as Related to Busy Beaver Numbers
por: Tandi, Gurpreet, et al.
Publicado: (2026)