Cited in
(only showing first 100 items - show all)- Diophantine
- Graph Theory
- PairingHeap
- Psi-calculi
- Skew Heap
- Regular Sets
- SAT Solver Verification
- Hotel Key Card
- Splay Tree
- Stable Matching
- Verified Prover
- Slicing
- Worker/Wrapper Transformation
- ProofPeer
- Dynamic Architectures
- FACTum
- XIsabelle
- FOL_Harrison
- Groebner_Bases
- GeoCoq
- Jape
- Vickrey_Clarke_Groves
- F5C
- Naproche-SAD
- Architectural_Design_Patterns
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- A formally verified proof of the central limit theorem
- Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing
- Verified interactive computation of definite integrals
- Theorem Proving in Higher Order Logics
- Towards verified handwritten calculational proofs (short paper)
- Towards formal foundations for game theory
- Refinement-Based Verification of Interactive Real-Time Systems
- Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
- A comparison of Mizar and Isar
- OCRA
- Theories as types
- Interactive theorem proving from the perspective of Isabelle/Isar
- A mechanized proof of the basic perturbation lemma
- From LCF to Isabelle/HOL
- Interaction with formal mathematical documents in Isabelle/PIDE
- scientific article; zbMATH DE number 2003161 (Why is no real title available?)
- Psi-calculi in Isabelle
- Locales: a module system for mathematical theories
- Correctness of Pointer Manipulating Algorithms Illustrated by a Verified BDD Construction
- HolPy
- jsCoq
- Proving pointer programs in higher-order logic
- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
- Constructive Type Classes in Isabelle
- UTPCalc -- a calculator for UTP predicates
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Semantics of Mizar as an Isabelle object logic
- Modelling algebraic structures and morphisms in ACL2
- From LTL to deterministic automata. A safraless compositional approach
- scientific article; zbMATH DE number 2003148 (Why is no real title available?)
- Partial and nested recursive function definitions in higher-order logic
- Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
- Improving legibility of natural deduction proofs is not trivial
- Proviola: a tool for proof re-animation
- From Tarski to Hilbert
- Amortized complexity verified
- An Isabelle proof method language
- Automated Reasoning in Higher-Order Regular Algebra
- A vernacular for coherent logic
- Automation for interactive proof: first prototype
- Complex_Geometry
- Poincare_Disc
- A formally verified solver for homogeneous linear Diophantine equations
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Smooth_Manifolds
- A consistent foundation for Isabelle/HOL
- Managing proof documents for asynchronous processing
- Interactive simplifier tracing and debugging in Isabelle
- A mechanised abstract formalisation of concept lattices
- Comprehending Isabelle/HOL’s Consistency
- scientific article; zbMATH DE number 1927415 (Why is no real title available?)
- Mathematical Knowledge Management
- The seventeen provers of the world. Foreword by Dana S. Scott..
- A hierarchy of semantics for non-deterministic term rewriting systems
- Tool-Based Verification of a Relational Vertex Coloring Program
- Building Formal Method Tools in the Isabelle/Isar Framework
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
- Pervasive parallelism in highly-trustable interactive theorem proving systems
- Interpreting mathematical texts in Naproche-SAD
- Relational and Kleene-Algebraic Methods in Computer Science
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Logic for Programming, Artificial Intelligence, and Reasoning
- Interactive verification of architectural design patterns in FACTum
- Automating theorem proving with SMT
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- On definitions of constants and types in HOL
- A generic and executable formalization of signature-based Gröbner basis algorithms
- Formalization of the Poincaré disc model of hyperbolic geometry
- The Isabelle Framework
- Merging Procedural and Declarative Proof
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
- A certified proof of the Cartan fixed point theorems
This page was built for software: Isabelle/Isar
