Cited in
(only showing first 100 items - show all)- A parallelized theorem prover for a logic with parallel execution
- Comprehending Isabelle/HOL’s Consistency
- Proof-producing reflection for HOL. With an application to model polymorphism
- scientific article; zbMATH DE number 1863382 (Why is no real title available?)
- scientific article; zbMATH DE number 1927415 (Why is no real title available?)
- Proving opacity of a pessimistic STM
- A new foundation for Nominal Isabelle
- Higher-order abstract syntax in Isabelle/HOL
- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
- Proof search with set variable instantiation in the calculus of constructions
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Formal reasoning under cached address translation
- A simple formalization and proof for the multilated chess board
- A hierarchy of semantics for non-deterministic term rewriting systems
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
- scientific article; zbMATH DE number 1863387 (Why is no real title available?)
- Structuring metatheory on inductive definitions
- A verified efficient implementation of the LLL basis reduction algorithm
- Turning Inductive into Equational Specifications
- Verified lightweight bytecode verification
- scientific article; zbMATH DE number 65526 (Why is no real title available?)
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- A New and Formalized Proof of Abstract Completion
- The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving
- Tool-Based Verification of a Relational Vertex Coloring Program
- A user-friendly interface for a lightweight verification system
- Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover's palette
- Graphical reasoning in compact closed categories for quantum computation
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- scientific article; zbMATH DE number 1222427 (Why is no real title available?)
- A logical framework combining model and proof theory
- Liveness Reasoning with Isabelle/HOL
- Mechanical proofs about BW multi-party contract signing protocol
- Formal verification of an executable LTL model checker with partial order reduction
- From types to sets by local type definition in higher-order logic
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Verifying OpenJDK's sort method for generic collections
- Confluence by decreasing diagrams -- formalized
- Conjecture synthesis for inductive theories
- Verification of dynamic bisimulation theorems in Coq
- scientific article; zbMATH DE number 2185692 (Why is no real title available?)
- The future of logic: foundation-independence
- Cardinals in Isabelle/HOL
- scientific article; zbMATH DE number 1424013 (Why is no real title available?)
- scientific article; zbMATH DE number 1424022 (Why is no real title available?)
- Building Formal Method Tools in the Isabelle/Isar Framework
- Integration of a Software Model Checker into Isabelle
- Stream Fusion for Isabelle’s Code Generator
- scientific article; zbMATH DE number 1956564 (Why is no real title available?)
- A formalization of Dedekind domains and class groups of global fields
- A formalization of the Smith normal form in higher-order logic
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- \textsc{Prawf}: an interactive proof system for program extraction
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Towards a trustworthy semantics-based language framework via proof generation
- Lyndon words formalized in Isabelle/HOL
- A framework for formal dynamic dependability analysis using HOL theorem proving
- Simple dataset for proof method recommendation in Isabelle/HOL
- MMTTeX: connecting content and narration-oriented document formats
- A realizability interpretation of Church's simple theory of types
- Mechanizing coinduction and corecursion in higher-order logic
- Reasoning about cardinalities of relations with applications supported by proof assistants
- scientific article; zbMATH DE number 1948157 (Why is no real title available?)
- Dynamic asset allocation in a mean-variance framework
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
- Efficient verification of imperative programs using auto2
- Imperative Functional Programming with Isabelle/HOL
- An approach to automatic deductive synthesis of functional programs
- Scalable fine-grained proofs for formula processing
- Certification of nonclausal connection tableaux proofs
- A scalable module system
- Levels of truth
- Experiments in causality and STIT
- 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
- Proving opacity via linearizability: a sound and complete method
- Isabelle formalization of set theoretic structures and set comprehensions
- FindFacts
- SErAPIS
- Practical probability: applying pGCL to lattice scheduling
- scientific article; zbMATH DE number 1722714 (Why is no real title available?)
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- The refinement calculus of reactive systems
- Specifying properties of dynamic architectures using configuration traces
- Faster and more complete extended static checking for the Java modeling language
- Proving linearizability with temporal logic
- scientific article; zbMATH DE number 1947524 (Why is no real title available?)
- Higher-Order Multi-Valued Resolution
- A practical implementation of simple consequence relations using inductive definitions
- A verified implementation of algebraic numbers in Isabelle/HOL
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- Balancing the load. Leveraging a semantics stack for systems verification
- Smart testing of functional programs in Isabelle
- Proof pearl: Mechanizing the textbook proof of Huffman's algorithm
- A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
- Belief revision, minimal change and relaxation: A general framework based on satisfaction systems, and applications to description logics
- Towards an awareness-based semantics for security protocol analysis
- Model-theoretic conservative extension for definitional theories
This page was built for software: Isabelle
