Interactive Theorem Proving | AMiner期刊详情 | AMiner

Interactive Theorem Proving | AMiner期刊详情 | AMiner

年发文量

研究主题

论文（686）

排序

时间引用

1Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean.

Eric Jonathan Wang, Elif Üsküplü

2026

引用

2Verification of the Garsia-Wachs Algorithm.

Makoto Kanazawa

2026

引用

3Certified Infinite Descent Criteria in Isabelle/HOL.

Jamie Wright,Liron Cohen,Reuben N. S. Rowe,Andrei Popescu

2026

引用

4Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL.

Fang Yan, Benoît Ballenghien,Simon Foster,Ana Cavalcanti, James Baxter,Burkhart Wolff

2026

引用

5Completing Almost Fair Simulations.

Arthur Correnson, Iona Kuhn,Bernd Finkbeiner

2026

引用

6Enhancing Interactive Theorem Prover Error Messages with Hints.

Maria Khakimova, Sára Juhosová, Jaro S. Reinders, Jesper Cockx

2026

引用

7Feedback & Synthesis in LLM-Assisted Termination Proofs.

Zeke Medley,Panagiotis Manolios

2026

引用

8Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees.

Yiming Lin, Ian Kariniemi, Yao Li

2026

引用

9Formalizing a Hoare Calculus for Choreographic Programming.

Luís Cruz-Filipe, Thomas Wulff Heissel

2026引用：1

引用

10Functional Correctness of an Optimized Modular Inversion Algorithm.

Assia Mahboubi,Guillaume Melquiond,Pierre-Yves Strub, Tomás Vallejos Parada

2026

引用

11Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language.

Vladimir Gladshtein,K. Rustan M. Leino

2026

引用

12Fractional Separation Logic in Isabelle LLVM.

2026

引用

13Developing a Quantum Crypto Theorem Prover from Scratch (invited Talk).

Dominique Unruh

2026

引用

14Nitro Isolation Engine: Formally Verifying a Production Hypervisor (invited Talk).

Hanno Becker,Nathan Chong,Robert Dockins, Jim Grundy, Jason Z. S. Hu, Ike Mulder,Dominic P. Mulligan, Paul Mure,Bryan Parno, Lawrence C. Paulson, Konrad Slind

2026

引用

15ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving.

Amitayush Thakur, George Tsoukalas,Greg Durrett,Swarat Chaudhuri

2026

引用

16Securing the Foundations of an Intermediate Language for Probabilistic Program Verification.

Oliver Bøving,Christoph Matheja

2026

引用

17Formal Primal-Dual Algorithm Analysis (short Paper).

Mohammad Abdulaziz, Thomas Ammer, Christoph Madlener

2026

引用

18Lazy Proof Automation for Separation Logic.

Valentin Mikhalchuk, Vladimir Gladshtein,Ilya Sergey

2026

引用

19130K Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (short Paper).

2026

引用

20From Weierstraß to Dedekind Via Jacobi: Formalising Foundations of Modular Forms.

Manuel Eberl,Wenda Li,Lawrence C. Paulson

2026

引用

高被引作者

作者	引用	发文
Cyril Cohen	662	10
Assia Mahboubi	619	10
Enrico Tassi	595	6
Laurent Théry	563	5
Jasmin Blanchette	551	11
Jeremy Avigad	516	9
Georges Gonthier	512	4
Tobias Nipkow	486	15
Andrea Asperti	475	2
Yves Bertot	469	2

高产作者

作者	引用	发文
Magnus Myreen	315	17
Cezary Kaliszyk	261	15
Tobias Nipkow	486	15
Peter Lammich	385	14
Michael Norrish	90	13
Andreas Lochbihler	291	13
Josef Urban	300	12
Jasmin Blanchette	551	11
Assia Mahboubi	619	10
Dmitriy Traytel	231	10

相关期刊

European Joint Conferences on Theory And Practice of Software

Tools and Algorithms for Construction and Analysis of Systems

International Conference on Verification, Model Checking and Abstract Interpretation

European Symposium on Programming

International Symposium on Functional and Logic Programming

International Colloquium on Theoretical Aspects of Computing

Asian Symposium on Programming Languages and Systems

Automated Technology for Verification and Analysis

Principles and Practice of Declarative Programming

Certified Programs and Proofs