HOL

swMATH5492MaRDI QIDQ17631FDOQ17631

Author name not available (Why is that?)

Described by source

• A Brief Overview of HOL4

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