Cited in
(only showing first 100 items - show all)- Towards Self-verification of HOL Light
- Unifying Sets and Programs via Dependent Types
- Comprehending Isabelle/HOL’s Consistency
- Proof-producing reflection for HOL. With an application to model polymorphism
- scientific article; zbMATH DE number 2185701 (Why is no real title available?)
- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
- scientific article; zbMATH DE number 1927430 (Why is no real title available?)
- Proof search with set variable instantiation in the calculus of constructions
- 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
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
- Formal verification of integrity-preserving countermeasures against cache storage side-channels
- Structuring metatheory on inductive definitions
- A verified efficient implementation of the LLL basis reduction algorithm
- On the Formal Analysis of Geometrical Optics in HOL
- A New and Formalized Proof of Abstract Completion
- Theorem Proving in Higher Order Logics
- A String of Pearls: Proofs of Fermat's Little Theorem
- Tool-Based Verification of a Relational Vertex Coloring Program
- Characteristics of de Bruijn’s early proof checker Automath
- The 10th IJCAR automated theorem proving system competition -- CASC-J10
- Formal Analysis of Memory Contention in a Multiprocessor System
- Specification and automatic verification of self-timed queues
- Verification of a multiprocessor cache protocol using simulation relations and higher-order logic
- From types to sets by local type definition in higher-order logic
- Proof pearl: Bounding least common multiples with triangles
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Verification of dynamic bisimulation theorems in Coq
- The future of logic: foundation-independence
- Cardinals in Isabelle/HOL
- An approach to formal verification of human-computer interaction
- From the universality of mathematical truth to the interoperability of proof systems
- Guiding an automated theorem prover with neural rewriting
- Unique solutions of contractions, CCS, and their HOL formalisation
- A framework for formal dynamic dependability analysis using HOL theorem proving
- scientific article; zbMATH DE number 2185678 (Why is no real title available?)
- Simple dataset for proof method recommendation in Isabelle/HOL
- Wait-free linearization with a mechanical proof
- scientific article; zbMATH DE number 3991418 (Why is no real title available?)
- A realizability interpretation of Church's simple theory of types
- An algebraic approach to compiler design
- Reasoning about cardinalities of relations with applications supported by proof assistants
- On the desirability of mechanizing calculational proofs
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
- Scalable fine-grained proofs for formula processing
- Formal verification of a partial-order reduction technique for model checking
- 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
- Proof assistance for real-time systems using an interactive theorem prover
- Formal Analysis of Optical Waveguides in HOL
- FindFacts
- SErAPIS
- Extended Static Checking by Calculation Using the Pointfree Transform
- Tree neural networks in HOL4
- Two case studies of semantics execution in Maude: CCS and LOTOS
- Journeys in non-classical computation I: A grand challenge for computing research
- Unifying sets and programs via dependent types
- Automatic derivation of the irrationality of \(e\)
- Verified over-approximation of the diameter of propositionally factored transition systems
- Specifying properties of dynamic architectures using configuration traces
- scientific article; zbMATH DE number 1059330 (Why is no real title available?)
- Semantic essence of AsmL
- A verified implementation of algebraic numbers in Isabelle/HOL
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm
- Adapting functional programs to higher order logic
- Evaluation of anonymity and confidentiality protocols using theorem proving
- Formal reliability analysis of combinational circuits using theorem proving
- Reasoning about conditional probabilities in a higher-order-logic theorem prover
- Verifying the unification algorithm in LCF
- Deriving comparators and show functions in Isabelle/HOL
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- scientific article; zbMATH DE number 1424021 (Why is no real title available?)
- Towards Knowledge Management for HOL Light
- Pattern matches in HOL: a new representation and improved code generation
- Representing model theory in a type-theoretical logical framework
- scientific article; zbMATH DE number 1301861 (Why is no real title available?)
- Formalising Semantics for Expected Running Time of Probabilistic Programs
- Refinement to imperative HOL
- The foundation of a generic theorem prover
- Twenty Years of Theorem Proving for HOLs Past, Present and Future
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
- Theoretical Aspects of Computing - ICTAC 2004
- Theories for mechanical proofs of imperative programs
- scientific article; zbMATH DE number 1113859 (Why is no real title available?)
- scientific article; zbMATH DE number 1980938 (Why is no real title available?)
- Heterogeneous proofs: spider diagrams meet higher-order provers
- The seven virtues of simple type theory
- scientific article; zbMATH DE number 1863380 (Why is no real title available?)
- Formal dependability modeling and analysis: a survey
- Validating the PSL/Sugar semantics using automated reasoning
- A Formal Proof of Square Root and Division Elimination in Embedded Programs
- Automatic functional correctness proofs for functional search trees
- A formal quantifier elimination for algebraically closed fields
- Formalization of finite-state discrete-time Markov chains in HOL
- Using Structural Recursion for Corecursion
- Formal verification of a programming logic for a distributed programming language
This page was built for software: HOL
