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)

• 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\)
• Adapting functional programs to higher order logic
• Verifying the unification algorithm in LCF
• Title not available (Why is that?)
• A formal quantifier elimination for algebraically closed fields
• Exploring abstract algebra in constructive type theory
• 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
• 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
• Hybrid interactive theorem proving using Nuprl and HOL
• Theoretical Aspects of Computing – ICTAC 2005
• A complete axiom system for propositional projection temporal logic with cylinder computation model
• Stateless higher-order logic with quantified types
• 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?)
• Annotations in formal specifications and proofs
• Modeling multi-rate DSP specification semantics for formal transformational design in HOL
• Using theorem proving to verify expectation and variance for discrete random variables
• Proof assistants: history, ideas and future
• Algebraic models of correctness for abstract pipelines.
• The verified software repository: a step towards the verifying compiler
• Formal kinematic analysis of a general 6R manipulator using the screw theory
• Title not available (Why is that?)
• Algebraic models of microprocessors architecture and organisation
• Formalization of entropy measures in HOL
• A mechanical analysis of program verification strategies
• Unifying theories in ProofPower-Z
• The higher-order-logic Formath
• Proof producing synthesis of arithmetic and cryptographic hardware
• A new application for explanation-based generalisation within automated deduction
• A consistent foundation for Isabelle/HOL
• A consistent foundation for Isabelle/HOL
• Cardinals in Isabelle/HOL
• 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
• 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
• Verified over-approximation of the diameter of propositionally factored transition systems
• Formalising Semantics for Expected Running Time of Probabilistic Programs
• Refinement to imperative HOL
• Rewriting, inference, and proof
• Using Structural Recursion for Corecursion
• Formal analysis of the kinematic Jacobian in screw theory
• Reuse of proofs in software verification
• Mechanized metatheory revisited
• Formalizing axiomatic systems for propositional logic in Isabelle/HOL
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
• Formalizing an analytic proof of the prime number theorem
• Incorporating quotation and evaluation into Church's type theory
• Formal Methods in Computer-Aided Design
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
• Formalization of function matrix theory in HOL
• A verified algorithm enumerating event structures
• Formalization of linear space theory in the higher-order logic proving system
• What's in a theorem name?
• Hoare Logic for Realistically Modelled Machine Code
• Formally verified algorithms for upper-bounding state space diameters
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Formal Reasoning About Causality Analysis
• Mechanizing the metatheory of Sledgehammer
• Title not available (Why is that?)
• A verified enclosure for the Lorenz attractor (rough diamond)
• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
• The formalization of discrete Fourier transform in HOL
• On the Formalization of Z-Transform in HOL
• Formalization of fractional order PD control systems in HOL4

This page was built for software: HOL