On the public citation graph

QED at Large: A Survey of Engineering of Formally Verified Software

https://doi.org/10.1561/2500000045
0 signed · 483 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1002/9780470050118.ecse579openalex-snapshot
Proofs of Correctness in Mathematics and Industry
inferredcites →https://doi.org/10.1006/inco.1994.1013openalex-snapshot
An Extension of System F with Subtyping
inferredcites →https://doi.org/10.1006/jsco.1997.0171openalex-snapshot
A Generic Approach to Building User Interfaces for Theorem Provers
inferredcites →https://doi.org/10.1006/jsco.1997.0175openalex-snapshot
Interactive Theorem Proving: An Empirical Study of User Activity
inferredcites →https://doi.org/10.1006/jsco.2002.0552openalex-snapshot
A Constructive Algebraic Hierarchy in Coq
inferredcites →https://doi.org/10.1007/10930755_14openalex-snapshot
Program Extraction from Large Proof Developments
inferredcites →https://doi.org/10.1007/10930755_18openalex-snapshot
Implementing Modules in the Coq System
inferredcites →https://doi.org/10.1007/11541868_18openalex-snapshot
Extensionality in the Calculus of Constructions
inferredcites →https://doi.org/10.1007/11541868_4openalex-snapshot
Mechanized Metatheory for the Masses: The PoplMark Challenge
inferredcites →https://doi.org/10.1007/11541868_7openalex-snapshot
Proving Equalities in a Commutative Ring Done Right in Coq
inferredcites →https://doi.org/10.1007/11541868_9openalex-snapshot
A Design Structure for Higher Order Quotients
inferredcites →https://doi.org/10.1007/11542384openalex-snapshot
The Seventeen Provers of the World
inferredcites →https://doi.org/10.1007/11617990_10openalex-snapshot
A Tool for Automated Theorem Proving in Agda
inferredcites →https://doi.org/10.1007/11617990_2openalex-snapshot
A Content Based Mathematical Search Engine: Whelp
inferredcites →https://doi.org/10.1007/11812289_3openalex-snapshot
Structured Induction Proofs in Isabelle/Isar
inferredcites →https://doi.org/10.1007/11812289_4openalex-snapshot
Interpretation of Locales in Isabelle: Theories and Proof Contexts
inferredcites →https://doi.org/10.1007/3-540-09724-4openalex-snapshot
Edinburgh LCF
inferredcites →https://doi.org/10.1007/3-540-13346-1_10openalex-snapshot
Deriving structural induction in LCF
inferredcites →https://doi.org/10.1007/3-540-15983-5_13openalex-snapshot
Constructions: A higher order proof system for mechanizing mathematics
inferredcites →https://doi.org/10.1007/3-540-39185-1_12openalex-snapshot
A New Extraction for Coq
inferredcites →https://doi.org/10.1007/3-540-44404-1_7openalex-snapshot
A Tactic Language for the System Coq
inferredcites →https://doi.org/10.1007/3-540-44755-5_18openalex-snapshot
Refinement Calculus for Logic Programming in Isabelle/HOL
inferredcites →https://doi.org/10.1007/3-540-44755-5_26openalex-snapshot
Mizar Light for HOL Light
inferredcites →https://doi.org/10.1007/3-540-44802-0_1openalex-snapshot
Local Reasoning about Programs that Alter Data Structures
inferredcites →https://doi.org/10.1007/3-540-45315-6_4openalex-snapshot
Type Isomorphisms and Proof Reuse in Dependent Type Theory
inferredcites →https://doi.org/10.1007/3-540-45685-6_3openalex-snapshot
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction
inferredcites →https://doi.org/10.1007/3-540-45685-6_4openalex-snapshot
Efficient Reasoning about Executable Specifications in Coq
inferredcites →https://doi.org/10.1007/3-540-45842-5_12openalex-snapshot
Changing Data Structures in Type Theory: A Study of Natural Numbers
inferredcites →https://doi.org/10.1007/3-540-45842-5_13openalex-snapshot
Elimination with a Motive
inferredcites →https://doi.org/10.1007/3-540-45842-5_2openalex-snapshot
Executing Higher Order Logic
inferredcites →https://doi.org/10.1007/3-540-45842-5_7openalex-snapshot
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals
inferredcites →https://doi.org/10.1007/3-540-46419-0_3openalex-snapshot
Proof General: A Generic Tool for Proof Development
inferredcites →https://doi.org/10.1007/3-540-48256-3_11openalex-snapshot
Locales A Sectioning Concept for Isabelle
inferredcites →https://doi.org/10.1007/3-540-48256-3_21openalex-snapshot
Integrating Gandalf and HOL
inferredcites →https://doi.org/10.1007/3-540-48256-3_3openalex-snapshot
Inductive Datatypes in HOL — Lessons Learned in Formal-Logic Engineering
inferredcites →https://doi.org/10.1007/3-540-48660-7_14openalex-snapshot
System Description: Twelf — A Meta-Logical Framework for Deductive Systems
inferredcites →https://doi.org/10.1007/3-540-52335-9_47openalex-snapshot
Inductively defined types
inferredcites →https://doi.org/10.1007/3-540-57826-9_152openalex-snapshot
A mechanisation of name-carrying syntax up to alpha-conversion
inferredcites →https://doi.org/10.1007/3-540-57826-9_154openalex-snapshot
AC unification in HOL90
inferredcites →https://doi.org/10.1007/3-540-57887-0_94openalex-snapshot
Proof by pointing
inferredcites →https://doi.org/10.1007/3-540-58085-9_72openalex-snapshot
Infinite objects in type theory
inferredcites →https://doi.org/10.1007/3-540-58156-1_17openalex-snapshot
A mechanically proof-checked encyclopedia of mathematics: Should we build one? Can we?
inferredcites →https://doi.org/10.1007/3-540-58216-9_25openalex-snapshot
Generalization and reuse of tactic proofs
inferredcites →https://doi.org/10.1007/3-540-58450-1_37openalex-snapshot
First-order automation for higher-order-logic theorem proving
inferredcites →https://doi.org/10.1007/3-540-60275-5_74openalex-snapshot
A new interface for HOL — Ideas, issues and implementation
inferredcites →https://doi.org/10.1007/3-540-60579-7_3openalex-snapshot
Codifying guarded definitions with recursive schemes
inferredcites →https://doi.org/10.1007/3-540-60579-7_8openalex-snapshot
On extensibility of proof checkers
inferredcites →https://doi.org/10.1007/3-540-61780-9_58openalex-snapshot
Implicit coercions in type systems
inferredcites →https://doi.org/10.1007/3-540-61780-9_59openalex-snapshot
A two-level approach towards lean proof-checking
inferredcites →https://doi.org/10.1007/3-540-61780-9_64openalex-snapshot
Automating inversion of inductive predicates in Coq
inferredcites →https://doi.org/10.1007/3-540-63104-6_7openalex-snapshot
Integration of automated and interactive theorem proving in ILF
inferredcites →https://doi.org/10.1007/978-1-4471-3240-0_7openalex-snapshot
Program Refinement by Theorem Prover
inferredcites →https://doi.org/10.1007/978-1-4471-3756-6_7openalex-snapshot
Refinement Diagrams
inferredcites →https://doi.org/10.1007/978-1-4612-6315-9_10openalex-snapshot
Proof of a Program: FIND
inferredcites →https://doi.org/10.1007/978-1-4614-1129-1_9openalex-snapshot
A Revision of the Proof of the Kepler Conjecture
inferredcites →https://doi.org/10.1007/978-3-319-00966-7_1openalex-snapshot
Foundations of Mathematics from the Perspective of Computer Verification
inferredcites →https://doi.org/10.1007/978-3-319-03545-1_10openalex-snapshot
Refinements for Free!
inferredcites →https://doi.org/10.1007/978-3-319-03545-1_9openalex-snapshot
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
inferredcites →https://doi.org/10.1007/978-3-319-06410-9_2openalex-snapshot
Proof Engineering Considered Essential
inferredcites →https://doi.org/10.1007/978-3-319-06410-9_4openalex-snapshot
40 Years of Formal Methods
inferredcites →https://doi.org/10.1007/978-3-319-08434-3_20openalex-snapshot
Matching Concepts across HOL Libraries
inferredcites →https://doi.org/10.1007/978-3-319-08434-3_9openalex-snapshot
Hipster: Integrating Theory Exploration in a Proof Assistant
inferredcites →https://doi.org/10.1007/978-3-319-08970-6_3openalex-snapshot
Towards a Formally Verified Proof Assistant
inferredcites →https://doi.org/10.1007/978-3-319-08970-6_32openalex-snapshot
Universe Polymorphism in Coq
inferredcites →https://doi.org/10.1007/978-3-319-08970-6_33openalex-snapshot
Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
inferredcites →https://doi.org/10.1007/978-3-319-10542-0openalex-snapshot
Concrete Semantics: With Isabelle/HOL
inferredcites →https://doi.org/10.1007/978-3-319-15201-1_1openalex-snapshot
A Usability Evaluation of Interactive Theorem Provers Using Focus Groups
inferredcites →https://doi.org/10.1007/978-3-319-19797-5_13openalex-snapshot
Turing-Completeness Totally Free
inferredcites →https://doi.org/10.1007/978-3-319-20615-8_1openalex-snapshot
Mining the Archive of Formal Proofs
inferredcites →https://doi.org/10.1007/978-3-319-22102-1_11openalex-snapshot
Proof-Producing Reflection for HOL
inferredcites →https://doi.org/10.1007/978-3-319-22102-1_17openalex-snapshot
Refinement to Imperative/HOL
inferredcites →https://doi.org/10.1007/978-3-319-22102-1_22openalex-snapshot
Foundational Property-Based Testing
inferredcites →https://doi.org/10.1007/978-3-319-22102-1_24openalex-snapshot
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
inferredcites →https://doi.org/10.1007/978-3-319-40229-1_8openalex-snapshot
Congruence Closure in Intensional Type Theory
inferredcites →https://doi.org/10.1007/978-3-319-43144-4_20openalex-snapshot
A Framework for the Automatic Formal Verification of Refinement from Cogent to C
inferredcites →https://doi.org/10.1007/978-3-319-43144-4_28openalex-snapshot
What’s in a Theorem Name?
inferredcites →https://doi.org/10.1007/978-3-319-43144-4_32openalex-snapshot
CoqPIE: An IDE Aimed at Improving Proof Development Productivity
inferredcites →https://doi.org/10.1007/978-3-319-62075-6_7openalex-snapshot
Classification of Alignments Between Concepts of Formal Mathematical Systems
inferredcites →https://doi.org/10.1007/978-3-319-63046-5_32openalex-snapshot
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
inferredcites →https://doi.org/10.1007/978-3-319-66107-0_1openalex-snapshot
Automated Theory Exploration for Interactive Theorem Proving:
inferredcites →https://doi.org/10.1007/978-3-319-66107-0_2openalex-snapshot
Automating Formalization by Statistical and Semantic Parsing of Mathematics
inferredcites →https://doi.org/10.1007/978-3-319-66167-4_1openalex-snapshot
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
inferredcites →https://doi.org/10.1007/978-3-319-70096-0_1openalex-snapshot
Tree-Structure CNN for Automated Theorem Proving
inferredcites →https://doi.org/10.1007/978-3-319-71237-6_14openalex-snapshot
Safety and Liveness of MCS Lock—Layer by Layer
inferredcites →https://doi.org/10.1007/978-3-319-89884-1_35openalex-snapshot
A Verified Compiler from Isabelle/HOL to CakeML
inferredcites →https://doi.org/10.1007/978-3-319-89960-2_4openalex-snapshot
Verified Model Checking of Timed Automata
inferredcites →https://doi.org/10.1007/978-3-319-94821-8_2openalex-snapshot
Towards Certified Meta-Programming with Typed Template-Coq
inferredcites →https://doi.org/10.1007/978-3-540-24725-8_26openalex-snapshot
Functors for Proofs and Programs
inferredcites →https://doi.org/10.1007/978-3-540-30142-4_12openalex-snapshot
Theorem Reuse by Proof Term Transformation
inferredcites →https://doi.org/10.1007/978-3-540-30142-4_17openalex-snapshot
A Decision Procedure for Geometry in Coq
inferredcites →https://doi.org/10.1007/978-3-540-30142-4_4openalex-snapshot
Proof Reuse with Extended Inductive Types
inferredcites →https://doi.org/10.1007/978-3-540-45085-6_10openalex-snapshot
Proving Pointer Programs in Higher-Order Logic
inferredcites →https://doi.org/10.1007/978-3-540-45085-6_22openalex-snapshot
IsaPlanner: A Prototype Proof Planner in Isabelle
inferredcites →https://doi.org/10.1007/978-3-540-68103-8_5openalex-snapshot
A Declarative Language for the Coq Proof Assistant
inferredcites →https://doi.org/10.1007/978-3-540-69407-6_39openalex-snapshot
Extraction in Coq: An Overview
inferredcites →https://doi.org/10.1007/978-3-540-71067-7_23openalex-snapshot
First-Class Type Classes
inferredcites →https://doi.org/10.1007/978-3-540-74105-3openalex-snapshot
Decision Procedures: An Algorithmic Point of View
inferredcites →https://doi.org/10.1007/978-3-540-74113-8openalex-snapshot
The Calculus of Computation: Decision Procedures with Applications to Verification
inferredcites →https://doi.org/10.1007/978-3-540-74464-1_11openalex-snapshot
Constructive Type Classes in Isabelle
inferredcites →https://doi.org/10.1007/978-3-540-74464-1_5openalex-snapshot
Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
inferredcites →https://doi.org/10.1007/978-3-540-78739-6_1openalex-snapshot
A Sound Semantics for OCaml light
inferredcites →https://doi.org/10.1007/978-3-642-02444-3_10openalex-snapshot
Local Theory Specifications in Isabelle/Isar
inferredcites →https://doi.org/10.1007/978-3-642-03359-9_23openalex-snapshot
Packaging Mathematical Structures
inferredcites →https://doi.org/10.1007/978-3-642-03359-9_24openalex-snapshot
Practical Tactics for Separation Logic
inferredcites →https://doi.org/10.1007/978-3-642-03359-9_30openalex-snapshot
A Hoare Logic for the State Monad
inferredcites →https://doi.org/10.1007/978-3-642-04222-5_18openalex-snapshot
Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
inferredcites →https://doi.org/10.1007/978-3-642-12251-4_9openalex-snapshot
Code Generation via Higher-Order Rewrite Systems
inferredcites →https://doi.org/10.1007/978-3-642-14052-5_11openalex-snapshot
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
inferredcites →https://doi.org/10.1007/978-3-642-14052-5_17openalex-snapshot
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
inferredcites →https://doi.org/10.1007/978-3-642-14052-5_18openalex-snapshot
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
inferredcites →https://doi.org/10.1007/978-3-642-14052-5_29openalex-snapshot
Equations: A Dependent Pattern-Matching Compiler
inferredcites →https://doi.org/10.1007/978-3-642-15260-3openalex-snapshot
Introduction to Reliable and Secure Distributed Programming
inferredcites →https://doi.org/10.1007/978-3-642-17511-4_20openalex-snapshot
Dafny: An Automatic Program Verifier for Functional Correctness
inferredcites →https://doi.org/10.1007/978-3-642-19718-5_1openalex-snapshot
Verified Software Toolchain
inferredcites →https://doi.org/10.1007/978-3-642-19718-5_25openalex-snapshot
General Bindings and Alpha-Equivalence in Nominal Isabelle
inferredcites →https://doi.org/10.1007/978-3-642-19829-8_17openalex-snapshot
A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs
inferredcites →https://doi.org/10.1007/978-3-642-24364-6_2openalex-snapshot
Automatic Proof and Disproof in Isabelle/HOL
inferredcites →https://doi.org/10.1007/978-3-642-25379-9_14openalex-snapshot
Tactics for Reasoning Modulo AC in Coq
inferredcites →https://doi.org/10.1007/978-3-642-28869-2_20openalex-snapshot
Validating LR(1) Parsers
inferredcites →https://doi.org/10.1007/978-3-642-31365-3_30openalex-snapshot
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
inferredcites →https://doi.org/10.1007/978-3-642-31374-5_3openalex-snapshot
Challenges and Experiences in Managing Large-Scale Proofs
inferredcites →https://doi.org/10.1007/978-3-642-31374-5_38openalex-snapshot
Isabelle/jEdit – A Prover IDE within the PIDE Framework
inferredcites →https://doi.org/10.1007/978-3-642-32347-8_25openalex-snapshot
A Language of Patterns for Subterm Selection
inferredcites →https://doi.org/10.1007/978-3-642-35308-6_10openalex-snapshot
The New Quickcheck for Isabelle
inferredcites →https://doi.org/10.1007/978-3-642-39320-4_28openalex-snapshot
ML4PG in Computer Algebra Verification
inferredcites →https://doi.org/10.1007/978-3-642-39320-4_29openalex-snapshot
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_10openalex-snapshot
Data Refinement in Isabelle/HOL
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_14openalex-snapshot
A Machine-Checked Proof of the Odd Order Theorem
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_17openalex-snapshot
Pragmatic Quotient Types in Coq
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_30openalex-snapshot
Shared-Memory Multiprocessing for Interactive Theorem Proving
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_5openalex-snapshot
Canonical Structures for the Working Coq User
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_6openalex-snapshot
MaSh: Machine Learning for Sledgehammer
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_8openalex-snapshot
Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_9openalex-snapshot
Automatic Data Refinement
inferredcites →https://doi.org/10.1007/978-3-642-39799-8_31openalex-snapshot
A Fully Verified Executable LTL Model Checker
inferredcites →https://doi.org/10.1007/978-3-642-41582-1_10openalex-snapshot
Engineering Proof by Reflection in Agda
inferredcites →https://doi.org/10.1007/978-3-642-45221-5_27openalex-snapshot
Proof-Pattern Recognition and Lemma Discovery in ACL2
inferredcites →https://doi.org/10.1007/978-3-642-45221-5_52openalex-snapshot
Polar: A Framework for Proof Refactoring
inferredcites →https://doi.org/10.1007/978-3-642-54833-8_16openalex-snapshot
Communicating State Transition Systems for Fine-Grained Concurrent Resources
inferredcites →https://doi.org/10.1007/978-3-642-54833-8_9openalex-snapshot
Impredicative Concurrent Abstract Predicates
inferredcites →https://doi.org/10.1007/978-3-642-61667-9openalex-snapshot
Constructive Analysis
inferredcites →https://doi.org/10.1007/978-3-662-07964-5openalex-snapshot
Interactive Theorem Proving and Program Development
inferredcites →https://doi.org/10.1007/978-3-662-43613-4_3openalex-snapshot
Formal Specification and Verification of CRDTs
inferredcites →https://doi.org/10.1007/978-3-662-48899-7_26openalex-snapshot
Sharing HOL4 and HOL Light Proof Knowledge
inferredcites →https://doi.org/10.1007/978-3-662-49224-6_6openalex-snapshot
Refactoring Proofs with Tactician
inferredcites →https://doi.org/10.1007/978-3-662-49498-1_21openalex-snapshot
Extensible and Efficient Automation Through Reflective Tactics
inferredcites →https://doi.org/10.1007/978-3-662-49665-7_19openalex-snapshot
Towards Formal Proof Metrics
inferredcites →https://doi.org/10.1007/978-94-011-1793-7_4openalex-snapshot
Assigning Meanings to Programs
inferredcites →https://doi.org/10.1007/978-94-017-0435-9_8openalex-snapshot
Proof Analysis, Generalization and Reuse
inferredcites →https://doi.org/10.1007/bf00244460openalex-snapshot
Productive use of failure in inductive proof
inferredcites →https://doi.org/10.1007/bf00291051openalex-snapshot
A calculus of refinements for program derivations
inferredcites →https://doi.org/10.1007/bf01696781openalex-snapshot
Die Vollständigkeit der Axiome des logischen Funktionenkalküls
inferredcites →https://doi.org/10.1007/bf01700692openalex-snapshot
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
inferredcites →https://doi.org/10.1007/bf01887212openalex-snapshot
Term rewriting and beyond — theorem proving in Isabelle
inferredcites →https://doi.org/10.1007/bfb0012826openalex-snapshot
The use of explicit plans to guide inductive proofs
inferredcites →https://doi.org/10.1007/bfb0012835openalex-snapshot
Computational metatheory in Nuprl
inferredcites →https://doi.org/10.1007/bfb0014565openalex-snapshot
Using reflection to build efficient and certified decision procedures
inferredcites →https://doi.org/10.1007/bfb0028401openalex-snapshot
Higher order quotients and their implementation in Isabelle HOL
inferredcites →https://doi.org/10.1007/bfb0030541openalex-snapshot
Isabelle
inferredcites →https://doi.org/10.1007/bfb0037116openalex-snapshot
Inductive definitions in the system Coq rules and properties
inferredcites →https://doi.org/10.1007/bfb0040259openalex-snapshot
Inductively defined types in the Calculus of Constructions
inferredcites →https://doi.org/10.1007/bfb0060623openalex-snapshot
The mathematical language AUTOMATH, its usage, and some of its extensions
inferredcites →https://doi.org/10.1007/bfb0060636openalex-snapshot
Constructive validity
inferredcites →https://doi.org/10.1007/bfb0097795openalex-snapshot
Inverting inductively defined relations in LEGO
inferredcites →https://doi.org/10.1007/bfb0105406openalex-snapshot
A mizar mode for HOL
inferredcites →https://doi.org/10.1007/s00454-009-9148-4openalex-snapshot
A Revision of the Proof of the Kepler Conjecture
inferredcites →https://doi.org/10.1007/s10009-002-0081-6openalex-snapshot
Proof engineering in the large: formal verification of Pentium�4 floating-point divider
inferredcites →https://doi.org/10.1007/s10009-017-0457-2openalex-snapshot
Coqoon
inferredcites →https://doi.org/10.1007/s10817-006-9027-0openalex-snapshot
“Rippling: Meta-Level Guidance for Mathematical Reasoning,” by Alan Bundy, David Basin, Dieter Hutter, and Andrew Ireland, Cambridge University Press, 2005
inferredcites →https://doi.org/10.1007/s10817-007-9070-5openalex-snapshot
User Interaction with the Matita Proof Assistant
inferredcites →https://doi.org/10.1007/s10817-008-9097-2openalex-snapshot
Nominal Techniques in Isabelle/HOL
inferredcites →https://doi.org/10.1007/s10817-008-9101-xopenalex-snapshot
Proof Synthesis and Reflection for Linear Arithmetic
inferredcites →https://doi.org/10.1007/s10817-010-9194-xopenalex-snapshot
Hybrid
inferredcites →https://doi.org/10.1007/s10817-011-9225-2openalex-snapshot
The Locally Nameless Representation
inferredcites →https://doi.org/10.1007/s10817-011-9226-1openalex-snapshot
A List-Machine Benchmark for Mechanized Metatheory
inferredcites →https://doi.org/10.1007/s10817-014-9303-3openalex-snapshot
Learning-Assisted Automated Reasoning with Flyspeck
inferredcites →https://doi.org/10.1007/s10817-015-9324-6openalex-snapshot
The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it)
inferredcites →https://doi.org/10.1007/s10817-015-9360-2openalex-snapshot
Eisbach: A Proof Method Language for Isabelle
inferredcites →https://doi.org/10.1007/s10817-016-9362-8openalex-snapshot
A Learning-Based Fact Selector for Isabelle/HOL
inferredcites →https://doi.org/10.1007/s10817-018-9454-8openalex-snapshot
A Consistent Foundation for Isabelle/HOL
inferredcites →https://doi.org/10.1007/s10817-018-9455-7openalex-snapshot
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
inferredcites →https://doi.org/10.1007/s10817-018-9457-5openalex-snapshot
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
inferredcites →https://doi.org/10.1007/s10817-018-9458-4openalex-snapshot
Hammer for Coq: Automation for Dependent Type Theory
inferredcites →https://doi.org/10.1007/s10817-018-9460-xopenalex-snapshot
Regular Language Representations in the Constructive Type Theory of Coq
inferredcites →https://doi.org/10.1007/s10817-018-9483-3openalex-snapshot
Mechanized Metatheory Revisited
inferredcites →https://doi.org/10.1007/s11225-006-6604-5openalex-snapshot
Program Extraction from Normalization Proofs
inferredcites →https://doi.org/10.1007/s11241-017-9286-3openalex-snapshot
High-assurance timing analysis for a high-assurance real-time operating system
inferredcites →https://doi.org/10.1007/s11786-014-0173-1openalex-snapshot
Recycling Proof Patterns in Coq: Case Studies
inferredcites →https://doi.org/10.1007/s11786-014-0182-0openalex-snapshot
HOL(y)Hammer: Online ATP Service for HOL Light
inferredcites →https://doi.org/10.1007/s12046-009-0001-5openalex-snapshot
Proof assistants: History, ideas and future
inferredcites →https://doi.org/10.1016/0304-3975(93)90095-bopenalex-snapshot
A type-theoretical alternative to ISWIM, CUCH, OWHY
inferredcites →https://doi.org/10.1016/0890-5401(88)90005-3openalex-snapshot
The calculus of constructions
inferredcites →https://doi.org/10.1016/1385-7258(72)90034-0openalex-snapshot
Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem
inferredcites →https://doi.org/10.1016/b978-0-12-386980-7.50019-8openalex-snapshot
Checking a Large Routine
inferredcites →https://doi.org/10.1016/b978-0-444-51624-4.50004-6openalex-snapshot
History of Interactive Theorem Proving
inferredcites →https://doi.org/10.1016/c2009-0-27982-7openalex-snapshot
Engineering a Compiler
inferredcites →https://doi.org/10.1016/j.entcs.2005.11.024openalex-snapshot
A Large-Scale Experiment in Executing Extracted Programs
inferredcites →https://doi.org/10.1016/j.entcs.2006.09.021openalex-snapshot
Web Interfaces for Proof Assistants
inferredcites →https://doi.org/10.1016/j.entcs.2007.01.018openalex-snapshot
A Head-to-Head Comparison of de Bruijn Indices and Names
inferredcites →https://doi.org/10.1016/j.entcs.2007.01.028openalex-snapshot
Nominal Reasoning Techniques in Coq
showing the first 200 of 434 · page through all 434

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.1007/978-3-030-53518-6_16openalex-snapshot
Maintaining a Library of Formal Mathematics
inferred← citeshttps://doi.org/10.1007/978-3-030-81688-9_37openalex-snapshot
Functional Correctness of C Implementations of Dijkstra’s, Kruskal’s, and Prim’s Algorithms
inferred← citeshttps://doi.org/10.1007/978-3-030-86261-9_1openalex-snapshot
A Theorem Proving Approach to Formal Verification of a Cognitive Agent
inferred← citeshttps://doi.org/10.1007/978-3-030-90138-7_2openalex-snapshot
Interactive Theorem Proving for Logic and Information
inferred← citeshttps://doi.org/10.1007/978-3-030-90870-6_4openalex-snapshot
Two Mechanisations of WebAssembly 1.0
inferred← citeshttps://doi.org/10.1007/978-3-031-19762-8_20openalex-snapshot
Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in Railway
inferred← citeshttps://doi.org/10.1007/978-3-031-29082-4_3openalex-snapshot
Curiously Empty Intersection of Proof Engineering and Computational Sciences
inferred← citeshttps://doi.org/10.1007/978-3-032-07021-0openalex-snapshot
Intelligent Computer Mathematics
inferred← citeshttps://doi.org/10.1007/978-3-032-07021-0_4openalex-snapshot
Growing Mathlib: maintenance of a large scale mathematical library
inferred← citeshttps://doi.org/10.1007/s10817-025-09735-8openalex-snapshot
Formally Verified Suffix Array Construction
inferred← citeshttps://doi.org/10.1007/s42979-020-00417-3openalex-snapshot
Verified Model Checking for Conjunctive Positive Logic
inferred← citeshttps://doi.org/10.1038/d41586-025-03585-5openalex-snapshot
Mathematicians put AI model AlphaProof to the test
inferred← citeshttps://doi.org/10.1109/access.2024.3414374openalex-snapshot
FABI: A Formal Analyzer of Binary Image Objects Identification Tools
inferred← citeshttps://doi.org/10.1109/ase.2019.00057openalex-snapshot
Mutation Analysis for Coq
inferred← citeshttps://doi.org/10.1109/correctness56720.2022.00007openalex-snapshot
Towards Verified Rounding Error Analysis for Stationary Iterative Methods
inferred← citeshttps://doi.org/10.1109/icse-companion58688.2023.00018openalex-snapshot
PRoofster: Automated Formal Verification
inferred← citeshttps://doi.org/10.1109/icse55347.2025.00033openalex-snapshot
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
inferred← citeshttps://doi.org/10.1109/sp40001.2021.00008openalex-snapshot
SoK: Computer-Aided Cryptography
inferred← citeshttps://doi.org/10.1109/sp54263.2024.00220openalex-snapshot
ARMOR: A Formally Verified Implementation of X.509 Certificate Chain Validation
inferred← citeshttps://doi.org/10.1109/tg.2023.3292982openalex-snapshot
Modeling Game Mechanics With Ceptre
inferred← citeshttps://doi.org/10.1145/3372885.3373817openalex-snapshot
Coq à la carte: a practical approach to modular syntax with binders
inferred← citeshttps://doi.org/10.1145/3372885.3373823openalex-snapshot
REPLica: REPL instrumentation for Coq analysis
inferred← citeshttps://doi.org/10.1145/3377812.3382156openalex-snapshot
mCoq
inferred← citeshttps://doi.org/10.1145/3453483.3454033openalex-snapshot
Proof repair across type equivalences
inferred← citeshttps://doi.org/10.1145/3497775.3503951openalex-snapshot
Coq’s vibrant ecosystem for verification engineering (invited talk)
inferred← citeshttps://doi.org/10.1145/3591221openalex-snapshot
Mostly Automated Proof Repair for Verified Libraries
inferred← citeshttps://doi.org/10.1145/3593374openalex-snapshot
Passport: Improving Automated Formal Verification Using Identifiers
inferred← citeshttps://doi.org/10.1145/3607844openalex-snapshot
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
inferred← citeshttps://doi.org/10.1145/3626252.3630928openalex-snapshot
Solving Proof Block Problems Using Large Language Models
inferred← citeshttps://doi.org/10.1145/3643763openalex-snapshot
Towards AI-Assisted Synthesis of Verified Dafny Methods
inferred← citeshttps://doi.org/10.1145/3664807openalex-snapshot
Code to Qed, the Project Manager's Guide to Proof Engineering
inferred← citeshttps://doi.org/10.1145/3689773openalex-snapshot
StarMalloc: Verifying a Modern, Hardened Memory Allocator
inferred← citeshttps://doi.org/10.1145/3691620.3695357openalex-snapshot
CoqPilot, a plugin for LLM-based generation of proofs
inferred← citeshttps://doi.org/10.1145/3715787openalex-snapshot
Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle
inferred← citeshttps://doi.org/10.1145/3720426openalex-snapshot
QED in Context: An Observation Study of Proof Assistant Users
inferred← citeshttps://doi.org/10.1145/3744916.3787783openalex-snapshot
ProofCoop: Collaborative Automated Formal Verification
inferred← citeshttps://doi.org/10.1145/3759425.3763391openalex-snapshot
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
inferred← citeshttps://doi.org/10.1145/3763068openalex-snapshot
Incremental Certified Programming
inferred← citeshttps://doi.org/10.1145/3763164openalex-snapshot
Proof Repair across Quotient Type Equivalences
inferred← citeshttps://doi.org/10.1145/3763181openalex-snapshot
On the Impact of Formal Verification on Software Development
inferred← citeshttps://doi.org/10.1145/3779132openalex-snapshot
Automatically Engineering Trusted Software: A Research Roadmap
inferred← citeshttps://doi.org/10.1145/3785652openalex-snapshot
Lessons from Formally Verified Deployed Software Systems
inferred← citeshttps://doi.org/10.1145/3803437.3805553openalex-snapshot
The Watermark Paradox: How Provenance Verification Paves the Road to Camouflaged Backdoors
inferredcites →https://doi.org/10.1561/2500000045openalex-snapshot
inferred← citeshttps://doi.org/10.15760/etd.7794openalex-snapshot
Using Intrinsically-Typed Definitional Interpreters to Verify Compiler Optimizations in a Monadic Intermediate Language
inferred← citeshttps://doi.org/10.2139/ssrn.7237460openalex-snapshot
Proof Engine Infrastructure: A Claim-graph Framework for AI-assisted Mathematical Research
inferred← citeshttps://doi.org/10.4204/eptcs.398.4openalex-snapshot
Towards Automatic Transformations of Coq Proof Scripts
inferred← citeshttps://doi.org/10.70675/5b3981d5zd1ecz4a42za770z3ef7f54f2c8fopenalex-snapshot
Integrating Automated Theorem Provers in Proof Assistants
inferred← citeshttps://doi.org/10.70675/7d8a27b4zebf6z43c3z9577zeaa9e6c64d97openalex-snapshot
Challenges in the collaborative evolution of a proof language and its ecosystem
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.