Joshua Clune

According to our database, Joshua Clune authored at least 15 papers between 2020 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2026

Hint-Based SMT Proof Reconstruction.

Joshua Clune, Haniel Barbosa, Jeremy Avigad

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2026

2025

Premise Selection for a Lean Hammer.

Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, Sean Welleck

CoRR, June, 2025

bv_decide SMT-COMP 2025 Submission.

Henrik Böving, Siddharth Bhat, Alex C. Keizer, Luisa Cicolini, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser

Dataset, June, 2025

bv_decide SMT-COMP 2025 Submission.

Henrik Böving, Siddharth Bhat, Alex C. Keizer, Luisa Cicolini, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser

Dataset, June, 2025

bv_decide SMT-COMP 2025 Submission.

Henrik Böving, Siddharth Bhat, Alex C. Keizer, Luisa Cicolini, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser

Dataset, June, 2025

bv_decide SMT-COMP 2025 Submission.

Henrik Böving, Siddharth Bhat, Alex C. Keizer, Luisa Cicolini, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser

Dataset, June, 2025

Artifact for Paper Lean-auto: An Interface between Lean 4 and Automated Theorem Provers.

Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad

Dataset, May, 2025

x86 Only Artifact for Paper Lean-auto: An Interface between Lean 4 and Automated Theorem Provers.

Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad

Dataset, April, 2025

Draft Artifact for Paper Lean-auto: An Interface between Lean 4 and Automated Theorem Provers.

Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad

Dataset, April, 2025

Interactive Bitvector Reasoning using Verified Bit-Blasting.

Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex C. Keizer, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser

Proc. ACM Program. Lang., 2025

Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers.

Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad

Proceedings of the Computer Aided Verification - 37th International Conference, 2025

2024

Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory.

Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2023

A Formalized Reduction of Keller's Conjecture.

Joshua Clune

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2020

Program equivalence for assisted grading of functional programs.

Joshua Clune, Vijay Ramamurthy, Ruben Martins, Umut A. Acar

Proc. ACM Program. Lang., 2020

Program Equivalence for Assisted Grading of Functional Programs (Extended Version).

Joshua Clune, Vijay Ramamurthy, Ruben Martins, Umut A. Acar

CoRR, 2020