Cited in
(only showing first 100 items - show all)- Proof assistant decision procedures for formalizing origami
- Comprehending Isabelle/HOL’s Consistency
- The Picard Algorithm for Ordinary Differential Equations in Coq
- scientific article; zbMATH DE number 1927415 (Why is no real title available?)
- A dyadic deontic logic in HOL
- Binding structures as an abstract data type
- Proving pointer programs in higher-order logic.
- Reasoning in Abella about structural operational semantics specifications
- A new foundation for Nominal Isabelle
- Higher-order abstract syntax in Isabelle/HOL
- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
- Generalized and formalized uncurrying
- A provably correct compilation of functional languages into scripting languages
- An assertional proof of the stability and correctness of Natural Mergesort
- Proof-producing synthesis of CakeML from monadic HOL functions
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Formal reasoning under cached address translation
- Why do the relativistic masses and momenta of faster-than-light particles decrease as their speeds increase?
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- An assertional proof of red-black trees using Dafny
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
- scientific article; zbMATH DE number 1863387 (Why is no real title available?)
- A verified efficient implementation of the LLL basis reduction algorithm
- Turning Inductive into Equational Specifications
- Verified lightweight bytecode verification
- Formal proof of a wave equation resolution scheme: the method error
- On the Formal Analysis of Geometrical Optics in HOL
- Constructing the views framework
- A New and Formalized Proof of Abstract Completion
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Type-theoretic approaches to ordinals
- Mechanically proving determinacy of hierarchical block diagram translations
- Solving quantifier-free first-order constraints over finite sets and binary relations
- Tool-Based Verification of a Relational Vertex Coloring Program
- Banishing ultrafilters from our consciousness
- Characteristics of de Bruijn’s early proof checker Automath
- Mechanizing \textit{Principia logico-metaphysica} in functional type-theory
- A logical framework combining model and proof theory
- Herbrand constructivization for automated intuitionistic theorem proving
- Liveness Reasoning with Isabelle/HOL
- Mechanical proofs about BW multi-party contract signing protocol
- A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation
- A formalization of metric spaces in HOL Light
- Formal verification of an executable LTL model checker with partial order reduction
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
- From types to sets by local type definition in higher-order logic
- Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Formalizing Scientifically Applicable Mathematics in a Definitional Framework
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Verifying a Compiler for Java Threads
- CoCon: a conference management system with formally verified document confidentiality
- The future of logic: foundation-independence
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Cardinals in Isabelle/HOL
- A framework for developing stand-alone certifiers
- scientific article; zbMATH DE number 1424013 (Why is no real title available?)
- scientific article; zbMATH DE number 1424022 (Why is no real title available?)
- Stream Fusion for Isabelle’s Code Generator
- scientific article; zbMATH DE number 1956564 (Why is no real title available?)
- Extending Sledgehammer with SMT solvers
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- A formalization of Dedekind domains and class groups of global fields
- A formalization of the Smith normal form in higher-order logic
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Binary codes that do not preserve primitivity
- From the universality of mathematical truth to the interoperability of proof systems
- Flexible proof production in an industrial-strength SMT solver
- Rensets and renaming-based recursion for syntax with bindings
- Formal analysis of multiparty contract signing
- Unique solutions of contractions, CCS, and their HOL formalisation
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- JEFL: joint embedding of formal proof libraries
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- Lyndon words formalized in Isabelle/HOL
- A framework for formal dynamic dependability analysis using HOL theorem proving
- Coming to terms with quantified reasoning
- Simple dataset for proof method recommendation in Isabelle/HOL
- From Sets to Bits in Coq
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Reasoning about cardinalities of relations with applications supported by proof assistants
- scientific article; zbMATH DE number 1948157 (Why is no real title available?)
- Tarski geometry axioms. III
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
- Efficient verification of imperative programs using auto2
- Imperative Functional Programming with Isabelle/HOL
- Certifying emptiness of timed Büchi automata
- EthVer: formal verification of randomized Ethereum smart contracts
- Scalable fine-grained proofs for formula processing
- Büchi automata optimisations formalised in Isabelle/HOL
- Experiments in causality and STIT
- From types to sets by local type definitions in higher-order logic
- A formal proof of Cauchy's residue theorem
- Algebraic numbers in Isabelle/HOL
- On the fine-structure of regular algebra
- scientific article; zbMATH DE number 2090132 (Why is no real title available?)
- FindFacts
This page was built for software: Isabelle/HOL
