Isabelle/HOL
From MaRDI portal
Software:14275
swMATH1569MaRDI QIDQ14275FDOQ14275
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Mechanizing \textit{Principia logico-metaphysica} in functional type-theory
- Herbrand constructivization for automated intuitionistic theorem proving
- Extending Sledgehammer with SMT solvers
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
- CoCon: a conference management system with formally verified document confidentiality
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- The future of logic: foundation-independence
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- Efficient verification of imperative programs using auto2
- On the fine-structure of regular algebra
- Maintaining a library of formal mathematics
- Metamath Zero: designing a theorem prover prover
- Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
- Collaborative Interactive Theorem Proving with Clide
- Lem: reusable engineering of real-world semantics
- Tools and Algorithms for the Construction and Analysis of Systems
- Mechanical Verification of a Constructive Proof for FLP
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)
- Grail: a functional form for imperative mobile code
- HOL Based First-Order Modal Logic Provers
- Specifying properties of concurrent computations in CLF
- WhyMP, a formally verified arbitrary-precision integer library
- Certification of Termination Proofs Using CeTA
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Formalizing the Logic-Automaton Connection
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- The Isabelle Framework
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Ivor, a Proof Engine
- The Abella Interactive Theorem Prover (System Description)
- Mining the Archive of Formal Proofs
- Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors
- Verifying a Hotel Key Card System
- Flyspeck I: Tame Graphs
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Ott: Effective tool support for the working semanticist
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Formal verification of monad transformers
- Automatic Data Refinement
- Binders unbound
- Analytic tableaux for higher-order logic with choice
- Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- Beginner's luck: a language for property-based generators
- General bindings and alpha-equivalence in Nominal Isabelle
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
- Amortized complexity verified
- SAD as a mathematical assistant -- how should we go from here to there?
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Psi-calculi in Isabelle
- Effect polymorphism in higher-order logic (proof pearl)
- Nominal techniques in Isabelle/HOL
- Using La\TeX\ as a semantic markup format
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Fixpoints and search in PVS
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Saoithín: a theorem prover for UTP
- The TPTP World -- infrastructure for automated reasoning
- Overview of the Mathemagix type system
- Termination of Isabelle functions via termination of rewriting
- The logic of \(U\cdot(TP)^{2}\)
- Bellerophon: tactical theorem proving for hybrid systems
- Hipster: integrating theory exploration in a proof assistant
- Experience report: seL4, formally verifying a high-performance microkernel
- Ynot: dependent types for imperative programs
- The Lean theorem prover (system description)
- ParaVerifier: an automatic framework for proving parameterized cache coherence protocols
- AUTO2, a saturation-based heuristic prover for higher-order logic
- LEO-II and Satallax on the Sledgehammer test bench
- Proof pearl: a probabilistic proof for the girth-chromatic number theorem
- A formally verified solver for homogeneous linear Diophantine equations
- ProofWatch: watchlist guidance for large theories in E
- ATPboost: learning premise selection in binary setting with ATP feedback
- The higher-order prover Leo-III
- Using the Isabelle ontology framework -- linking the formal with the informal
- Verified efficient implementation of Gabow's strongly connected component algorithm
- Unified decision procedures for regular expression equivalence
- Light-weight containers for Isabelle: efficient, extensible, nestable
- A formalized hierarchy of probabilistic system types. Proof pearl
- On logic embeddings and Gödel's God
- SEPIA: search for proofs using inferred automata
- A mechanized proof of loop freedom of the (untimed) AODV routing protocol
- A verified compiler for probability density functions
- Isabelle/UTP: a mechanised theory engineering framework
- Data refinement of invariant based programs
- Formalizing the Edmonds-Karp algorithm
- Friends with benefits. Implementing corecursion in foundational proof assistants
- A formal proof generator from semi-formal proof documents
- Coquelicot: a user-friendly library of real analysis for Coq
- Stone relation algebras
- TacticToe: learning to reason with HOL4 tactics
- RDA: a Coq library to reason about randomised distributed algorithms in the message passing model
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Certified reasoning with infinity
This page was built for software: Isabelle/HOL
