HOL
From MaRDI portal
Software:17631
swMATH5492MaRDI QIDQ17631FDOQ17631
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- A String of Pearls: Proofs of Fermat's Little Theorem
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
- Structuring metatheory on inductive definitions
- From the universality of mathematical truth to the interoperability of proof systems
- The Imandra Automated Reasoning System (System Description)
- The CADE-27 Automated theorem proving System Competition – CASC-27
- Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics
- Interactive verification of architectural design patterns in FACTum
- Machine-Checked Proof-Theory for Propositional Modal Logics
- Interpreting HOL in the calculus of constructions
- A generic and executable formalization of signature-based Gröbner basis algorithms
- An algebra of synchronous atomic steps
- Indentification of inductive properties during verification of synchronous sequential circuits
- Superposition with lambdas
- Specifying Properties of Dynamic Architectures Using Configuration Traces
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
- Machine learning guidance for connection tableaux
- Mechanisation of the AKS algorithm
- TacticToe: learning to prove with tactics
- Hoare-style logic for unstructured programs
- CryptHOL: game-based proofs in higher-order logic
- Title not available (Why is that?)
- Theory morphisms in Church's type theory with quotation and evaluation
- Verified analysis of random binary tree structures
- An Axiomatic Value Model for Isabelle/UTP
- Organizing numerical theories using axiomatic type classes
- Classification of finite fields with applications
- An Isabelle/HOL Formalisation of Green’s Theorem
- HOL Zero’s Solutions for Pollack-Inconsistency
- Formalization of functional variation in HOL Light
- Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL
- Verified analysis of random binary tree structures
- Backwards and forwards with separation logic
- Program verification in the presence of cached address translation
- Tactics and certificates in Meta Dedukti
- The verified CakeML compiler backend
- Equational Reasoning with Applicative Functors
- Standalone Tactics Using OpenTheory
- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
- Improved Tool Support for Machine-Code Decompilation in HOL4
- Goal-oriented conjecturing for Isabelle/HOL
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
- A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
- Unifying Theories in Isabelle/HOL
- Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP
- Induction with generalization in superposition reasoning
- From LCF to Isabelle/HOL
- An Isabelle/HOL formalisation of Green's theorem
- Formalization of geometric algebra in HOL Light
- The gauge integral theory in HOL4
- Mechanical verification of mutually recursive procedures
- Title not available (Why is that?)
- Circuits as streams in Coq: Verification of a sequential multiplier
- Title not available (Why is that?)
- Theorem Proving in Higher Order Logics
- Verification of dynamic bisimulation theorems in Coq
- An approach to formal verification of human-computer interaction
- On the desirability of mechanizing calculational proofs
- Automatic derivation of the irrationality of \(e\)
- Formalization of Entropy Measures in HOL
- Adapting functional programs to higher order logic
- Verifying the unification algorithm in LCF
- Title not available (Why is that?)
- Exploring abstract algebra in constructive type theory
- Hybrid interactive theorem proving using nuprl and HOL
- Formal verification of a programming logic for a distributed programming language
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automatic verification of cryptographic protocols with SETHEO
- Programmed strategies for program verification
- A Coq library for verification of concurrent programs
- Mechanizing Mathematical Reasoning
- Stateless Higher-Order Logic with Quantified Types
- A Consistent Foundation for Isabelle/HOL
- A theory of formal synthesis via inductive learning
- Theorem Proving in Higher Order Logics
- Title not available (Why is that?)
- Title not available (Why is that?)
- An intensional type theory: Motivation and cut-elimination
- A proof-centric approach to mathematical assistants
- Formalization of the standard uniform random variable
- An exercise in the automatic verification of asynchronous designs
- Exploiting parallelism: highly competitive semantic tree theorem prover
- A formalization of the LLL basis reduction algorithm
- Providing a formal linkage between MDG and HOL
- A few exercises in theorem processing
- A formal theory of simulations between infinite automata
- An embedding of timed transition systems in \(HOL\)
- Lazy techniques for fully expansive theorem proving
- The \(HOL\) logic extended with quantification over type variables
- Relational characterisations of paths
- Soundness and completeness proofs by coinductive methods
- Theoretical Aspects of Computing – ICTAC 2005
- A Formal Quantifier Elimination for Algebraically Closed Fields
- A complete axiom system for propositional projection temporal logic with cylinder computation model
- HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
- Formal probabilistic analysis of detection properties in wireless sensor networks
- Title not available (Why is that?)
- Title not available (Why is that?)
This page was built for software: HOL