Isabelle/Isar
From MaRDI portal
Software:14553
swMATH2006MaRDI QIDQ14553FDOQ14553
Author name not available (Why is that?)
Official website: http://isabelle.in.tum.de/Isar/
Cited In (only showing first 100 items - show all)
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Tool-Based Verification of a Relational Vertex Coloring Program
- Pervasive parallelism in highly-trustable interactive theorem proving systems
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
- Interpreting mathematical texts in Naproche-SAD
- Relational and Kleene-Algebraic Methods in Computer Science
- Logic for Programming, Artificial Intelligence, and Reasoning
- A synthesis of the procedural and declarative styles of interactive theorem proving
- The Isabelle Framework
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- On definitions of constants and types in HOL
- Automated Improving of Proof Legibility in the Mizar System
- A certified proof of the Cartan fixed point theorems
- KAT-ML: an interactive theorem prover for Kleene algebra with tests
- Verifying a Hotel Key Card System
- Supporting the formal verification of mathematical texts
- Local Theory Specifications in Isabelle/Isar
- A UTP semantic model for Orc language with execution status and fault handling
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Types for Proofs and Programs
- Types for Proofs and Programs
- Types for Proofs and Programs
- Using Isabelle/HOL to verify first-order relativity theory
- Title not available (Why is that?)
- Shortening of proof length is elusive for theorem provers
- Structured Induction Proofs in Isabelle/Isar
- Mechanical Theorem Proving in Tarski’s Geometry
- Dependently-typed formalisation of relation-algebraic abstractions
- An efficient Coq tactic for deciding Kleene algebras
- Structured formal development in Isabelle
- Jinja: towards a comprehensive formal semantics for a Java-like language
- Type classes and filters for mathematical analysis in Isabelle/HOL
- Relational characterisations of paths
- Mathematical method and proof
- A verified SAT solver framework with learn, forget, restart, and incrementality
- TkWinHOL
- MizarMode
- Isar
- Proof General
- Isabelle/ZF
- HOL-OCL
- Saoithin
- Isabelle/jEdit
- Isabelle/PIDE
- MathBrush
- Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing
- Theorem Proving in Higher Order Logics
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- KAT-ML
- ForMaRE
- EAT
- jEdit
- iJulienne
- PhoX
- FoCaLiZe
- Eisbach
- Refinement-Based Verification of Interactive Real-Time Systems
- A formally verified proof of the central limit theorem
- Verified interactive computation of definite integrals
- XBarnacle
- UTPCalc
- Slicing
- Worker/Wrapper Transformation
- ProofPeer
- A comparison of Mizar and Isar
- Interactive theorem proving from the perspective of Isabelle/Isar
- A mechanized proof of the basic perturbation lemma
- Title not available (Why is that?)
- Psi-calculi in Isabelle
- Locales: a module system for mathematical theories
- Proving pointer programs in higher-order logic
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Constructive Type Classes in Isabelle
- Title not available (Why is that?)
- 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
- Automated Reasoning in Higher-Order Regular Algebra
- An Isabelle proof method language
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Automation for interactive proof: first prototype
- Amortized complexity verified
- A formally verified solver for homogeneous linear Diophantine equations
- A mechanised abstract formalisation of concept lattices
- A consistent foundation for Isabelle/HOL
- Title not available (Why is that?)
- A hierarchy of semantics for non-deterministic term rewriting systems
- Building Formal Method Tools in the Isabelle/Isar Framework
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Complex_Geometry
- Poincare_Disc
- Automating theorem proving with SMT
- Interactive verification of architectural design patterns in FACTum
- A generic and executable formalization of signature-based Gröbner basis algorithms
- Formalization of the Poincaré disc model of hyperbolic geometry
- Merging Procedural and Declarative Proof
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
- Types for Proofs and Programs
This page was built for software: Isabelle/Isar