The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- Datatypes with shared selectors (Q1799121) (← links)
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions (Q1799129) (← links)
- Verified bytecode verifiers. (Q1874284) (← links)
- Verified bytecode verification and type-certifying compilation (Q1881665) (← links)
- Principles of proof scores in CafeOBJ (Q1929233) (← links)
- Left omega algebras and regular equations (Q1931903) (← links)
- In praise of algebra (Q1941861) (← links)
- Quantified multimodal logics in simple type theory (Q1945702) (← links)
- The locally nameless representation (Q1945914) (← links)
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (Q1945915) (← links)
- LEO-II and Satallax on the Sledgehammer test bench (Q1948289) (← links)
- Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L (Q1961917) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (Q1984794) (← links)
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (Q1984795) (← links)
- An assertional proof of red-black trees using Dafny (Q1984797) (← links)
- A verified proof checker for higher-order logic (Q1987736) (← links)
- Verifying minimum spanning tree algorithms with Stone relation algebras (Q1994364) (← links)
- On the semantics of polychronous polytimed specifications (Q1996008) (← links)
- Certifying emptiness of timed Büchi automata (Q1996011) (← links)
- (Co)inductive proof systems for compositional proofs in reachability logic (Q1996855) (← links)
- Unifying theories of reactive design contracts (Q2007732) (← links)
- Alloy*: a general-purpose higher-order relational constraint solver (Q2009609) (← links)
- A graph library for Isabelle (Q2018659) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- A generic and executable formalization of signature-based Gröbner basis algorithms (Q2028994) (← links)
- Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408) (← links)
- Mechanisation of the AKS algorithm (Q2031415) (← links)
- CoCon: a conference management system with formally verified document confidentiality (Q2031419) (← links)
- Automated proof of Bell-LaPadula security properties (Q2031424) (← links)
- Formalising \(\varSigma\)-protocols and commitment schemes using crypthol (Q2031427) (← links)
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (Q2031429) (← links)
- Proof-theoretic conservative extension of HOL with ad-hoc overloading (Q2037933) (← links)
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications (Q2037935) (← links)
- Formal verification of Ethereum smart contracts using Isabelle/HOL (Q2037985) (← links)
- Affine systems of ODEs in Isabelle/HOL for hybrid-program verification (Q2038037) (← links)
- Certifying Findel derivatives for blockchain (Q2043802) (← links)
- Towards satisfiability modulo parametric bit-vectors (Q2051567) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- A unifying splitting framework (Q2055869) (← links)
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- Verified interactive computation of definite integrals (Q2055881) (← links)
- The Isabelle/Naproche natural language proof assistant (Q2055899) (← links)
- Integration of formal proof into unified assurance cases with Isabelle/SACM (Q2065527) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Discovering and certifying lower bounds for the online bin stretching problem (Q2089680) (← links)
- Removing algebraic data types from constrained Horn clauses using difference predicates (Q2096439) (← links)
- Formalizing a Seligman-style tableau system for hybrid logic (short paper) (Q2096470) (← links)
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory (Q2102926) (← links)
