An Architecture for Interactive Program Provers
No abstract available.
Related papers
- AVATAR: The Architecture for First-Order Theorem Provers CAV 2014
- Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 TACAS 2025
- Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation POPL 2026
- Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP 2016
- Making sf IP=sf PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms CAV 2023
- Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice ICFP 2026
- A Comprehensive Specification and Verification of the L4 Microkernel API TACAS 2024
- A modular Isabelle framework for verifying saturation provers CPP 2021