Cover Image

Theorem Provers: One Size Fits All?

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Oates, Harrison, Yun, Hyeonggeun, Gurusinghe, Nikhila
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
by: Tang, Xichen
Published: (2025)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
by: Tsoukalas, George, et al.
Published: (2024)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
by: Li, Guchan, et al.
Published: (2026)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
by: Li, Jinzheng, et al.
Published: (2026)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
by: Vin, Eric, et al.
Published: (2025)

Expressive Power of One-Shot Control Operators and Coroutines
by: Kobayashi, Kentaro, et al.
Published: (2025)

Dynamic IFC Theorems for Free!
by: Algehed, Maximilian, et al.
Published: (2020)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
by: Shen, Ziju, et al.
Published: (2025)

A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics
by: Barthe, Gilles, et al.
Published: (2025)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
by: Jin, Xiangyu, et al.
Published: (2024)

Vibe Coding an LLM-powered Theorem Prover
by: Hou, Zhe
Published: (2026)

Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues
by: Allen, Bradley P.
Published: (2026)

Proof Recommendation System for the HOL4 Theorem Prover
by: Dekhil, Nour, et al.
Published: (2024)

An In-Context Learning Agent for Formal Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2023)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

A Probabilistic Choreography Language for PRISM
by: Carbone, Marco, et al.
Published: (2025)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

Positive Sharing and Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
by: Elad, Neta, et al.
Published: (2025)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

The Functional Machine Calculus III: Control
by: Heijltjes, Willem
Published: (2025)

Orthologic Type Systems
by: Guilloud, Simon, et al.
Published: (2025)

Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report)
by: Rowicki, Radosław Jan, et al.
Published: (2025)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Proceedings Twelfth Workshop on Fixed Points in Computer Science
by: Saurin, Alexis
Published: (2025)

A Lazy, Concurrent Convertibility Checker
by: Courant, Nathanaëlle, et al.
Published: (2025)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
by: Tsukada, Takeshi, et al.
Published: (2025)

Coinductive Proofs for Temporal Hyperliveness
by: Correnson, Arthur, et al.
Published: (2025)

Constructive characterisations of the must-preorder for asynchrony
by: Bernardi, Giovanni, et al.
Published: (2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Extended Abstract: Mutable Objects with Several Implementations
by: Kaufmann, Matt, et al.
Published: (2025)

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
by: Teuber, Samuel, et al.
Published: (2025)

Intrinsically Correct Algorithms and Recursive Coalgebras
by: Alexandru, Cass, et al.
Published: (2025)

Dependent Multiplicities in Dependent Linear Type Theory
by: Doré, Maximilian
Published: (2025)