HOL
From MaRDI portal
Cited in
(only showing first 100 items - show all)- HasCasl: integrated higher-order specification and program development
- Adapting functional programs to higher order logic
- Proof assistants: history, ideas and future
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Data compression for proof replay
- Using theorem proving to verify expectation and variance for discrete random variables
- Verifying the unification algorithm in LCF
- The notion of proof in hardware verification
- Higher-order rewrite systems and their confluence
- Theories for mechanical proofs of imperative programs
- ACL2
- Formal verification of a programming logic for a distributed programming language
- Coq
- The \(HOL\) logic extended with quantification over type variables
- Lazy techniques for fully expansive theorem proving
- Mechanizing some advanced refinement concepts
- A formal theory of simulations between infinite automata
- An embedding of timed transition systems in \(HOL\)
- HasCasl
- Set theory for verification. I: From foundations to functions
- IMPS: An interactive mathematical proof system
- Isabelle
- LEO-II
- An exercise in the automatic verification of asynchronous designs
- MetiTarski
- Constructing the real numbers in HOL
- Modeling multi-rate DSP specification semantics for formal transformational design in HOL
- Annotations in formal specifications and proofs
- Nitpick
- Ott
- Proviola
- lazyCoP
- solc-verify
- Wooki
- woot-haskell
- wootjs
- Woot
- RelView
- jsCoq
- HolPy
- Theorema
- TkWinHOL
- TPS
- ML
- Rapide
- Verification of the Miller-Rabin probabilistic primality test.
- A linear logical framework
- A rewriting approach to satisfiability procedures.
- Prosper
- Reuse of proofs in software verification
- Algebraic models of correctness for abstract pipelines.
- Isabelle/HOL
- FoCs
- CoFI
- ArcAngel
- CoqJVM
- Isabelle/Isar
- IsaPlanner
- PREVAIL
- LARCH
- VLISP
- ASTRAL
- OTTER
- VAMPIRE
- VESTA
- HOL/SPIN
- HOL-Z
- SPARK
- The calculus of constructions as a framework for proof search with set variable instantiation
- Proof-search in type-theoretic languages: An introduction
- RAISE
- THF0
- TCOZ
- Isabelle/HOL. A proof assistant for higher-order logic
- PVS
- Proof planning for strategy development
- Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
- Proof assistance for real-time systems using an interactive theorem prover
- Haskell
- Evaluating general purpose automated theorem proving systems
- MathWebSearch
- On the desirability of mechanizing calculational proofs
- Formal analysis of the kinematic Jacobian in screw theory
- SMV
- TPTP
- Aligning concepts across proof assistant libraries
- Metis
- Hammer for Coq: automation for dependent type theory
- Formally verified algorithms for upper-bounding state space diameters
- Formal kinematic analysis of a general 6R manipulator using the screw theory
- The formalization of discrete Fourier transform in HOL
- A theory of formal synthesis via inductive learning
- Isar
- MetaPRL
- Formalization of fractional order PD control systems in HOL4
- Mizar
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation
- FoCaLiZe and Dedukti to the rescue for proof interoperability
- Proof certificates in PVS
This page was built for software: HOL
