Isabelle/Isar

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