Isabelle/HOL: A Proof Assistant for Higher-Order Logic

By Tobias Nipkow, M. Wenzel, Lawrence C. Paulson. 2002

1,106 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/8064aa4544b6e3a81c5d651a7bdf801b0d3dc40c

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

The Isabelle Framework (2008, background): “Beginners are advised to start working with Isabelle/HOL; see the tutorial volume [30], and the companion tutorial [28] covering structured proofs.”
The Design and Implementation of Typed Scheme: From Scripts to Programs (2011, unknown): “PLT Redex programmers can write down a reduction semantics as easily as Isabelle/HOL programmers can write down typing rules.”
Building a push-button RESOLVE verifier: Progress and challenges (2011, unknown): “Like RESOLVE’s specification language, it is not limited to first-order logic, but instead supports higher-order logic (Isabelle/HOL [41]).”
A Survey on Ethereum Systems Security (2019, methodology): “ving to verify smart contracts at the EVM bytecode-level. Hirai [140] (D 23) took the ﬁrst step towards formalizing the EVM semantics,whichcanbeaccommodatedbyinteractivetheorem proverslikeIsabelle/HOL[141]toproveinvariantsandsafety propertiesofsmartcontracts.Amanietal.[142](D 24)extend the work in [”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, methodology): “Our main motivation for producing Alethe proofs is to leverage these proof reconstruction infrastructures, thus enabling the trustworthy integration of cvc5 in Isabelle/HOL and Coq.”
sFuzz: An Efficient Adaptive Fuzzer for Solidity Smart Contracts (2020, methodology): “acts formally by transforming the source code and the bytecode to F*, a language designed for verification [9]. In [17], the author presented an attempt to verify the Deed contract using Isabelle/HOL [26]. sFuzz is broadly related to work on analyzing smart contracts. In [13], Delmolino et al. showe”
A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols (2010, methodology): “More information about Isabelle/HOL can be found in [55, 56 ].”
A machine-checked model for a Java-like language, virtual machine, and compiler (2006, methodology): “Isabelle/HOL A Proof Assistant for Higher-Order Logic.”
The lean mathematical library (2019, methodology): “theorem provers [58]. 8.3 Libraries Based on Simple Type Theory A number of contemporary proof systems implement versions of simple type theory, among them HOL4 [55], HOL Light [35], and Isabelle/HOL [49]. In simple type theory, types and objects are separate things; one defines types and type const”