:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Bauer, Andrej, Park, Sewon, Simpson, Alex
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	https://arxiv.org/abs/2409.11946
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

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

Equivalence and Conditional Independence in Atomic Sheaf Logic
by: Simpson, Alex
Published: (2024)

Sheaves as oracle computations
by: Ahman, Danel, et al.
Published: (2026)

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

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

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

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

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

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

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

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

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

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

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

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

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

Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
by: Park, Sewon, et al.
Published: (2016)

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

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

Exact Exploration
by: Blass, Andreas, et al.
Published: (2024)

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

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

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

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

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

Bridging Computational Notions of Depth
by: Bienvenu, Laurent, et al.
Published: (2024)

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

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

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

Fixed Point Theorems in Computability Theory
by: Terwijn, Sebastiaan A.
Published: (2024)

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

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

Safety, Relative Tightness and the Probabilistic Frame Rule
by: Jereb, Janez Ignacij, et al.
Published: (2025)

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

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

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

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

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