Isabelle/Isar
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Isabelle
- jsCoq
- HolPy
- TkWinHOL
- Rapide
- MizarMode
- A UTP semantic model for Orc language with execution status and fault handling
- Isar
- A formally verified proof of the central limit theorem
- TAS
- Proof General
- Isabelle/ZF
- A consistent foundation for Isabelle/HOL
- HOL-OCL
- Towards verified handwritten calculational proofs (short paper)
- A formally verified solver for homogeneous linear Diophantine equations
- Towards formal foundations for game theory
- Theories as types
- Saoithin
- UTP2
- PIDE
- Isabelle/jEdit
- A comparison of Mizar and Isar
- Isabelle/PIDE
- MathBrush
- A generic and executable formalization of signature-based Gröbner basis algorithms
- Formalization of the Poincaré disc model of hyperbolic geometry
- RALL
- KAT-ML
- Verified interactive computation of definite integrals
- ForMaRE
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- EAT
- jEdit
- iJulienne
- PhoX
- ProofWeb
- Relational characterisations of paths
- Interpreting mathematical texts in Naproche-SAD
- From LCF to Isabelle/HOL
- Interaction with formal mathematical documents in Isabelle/PIDE
- Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
- Semantics of Mizar as an Isabelle object logic
- Poly/ML
- Interactive verification of architectural design patterns in FACTum
- Modelling algebraic structures and morphisms in ACL2
- Using Isabelle/HOL to verify first-order relativity theory
- Locales: a module system for mathematical theories
- From LTL to deterministic automata. A safraless compositional approach
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
- FoCaLiZe
- Automation for interactive proof: first prototype
- Locales
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
- Proving pointer programs in higher-order logic
- Eisbach
- RATH-Agda
- Metamath
- CC-Pi
- Xtext
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Translating Scala programs to Isabelle/HOL. System description
- Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
- Pervasive parallelism in highly-trustable interactive theorem proving systems
- From Tarski to Hilbert
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- On definitions of constants and types in HOL
- An Isabelle proof method language
- A synthesis of the procedural and declarative styles of interactive theorem proving
- PolyML
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- Automated Reasoning in Higher-Order Regular Algebra
- Improving legibility of natural deduction proofs is not trivial
- UTPCalc -- a calculator for UTP predicates
- Comprehending Isabelle/HOL’s Consistency
- Dependently-typed formalisation of relation-algebraic abstractions
- miz3
- Tutorial to locales and locale interpretation
- XBarnacle
- A hierarchy of semantics for non-deterministic term rewriting systems
- ltl2dstar
- Transfer
- Lifting
- WorkflowFM
- UTPCalc
- Structured formal development in Isabelle
- Tool-Based Verification of a Relational Vertex Coloring Program
- Building Formal Method Tools in the Isabelle/Isar Framework
- Verifying a Hotel Key Card System
- The Isabelle Framework
- Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
- scientific article; zbMATH DE number 5713654 (Why is no real title available?)
- Proviola: a tool for proof re-animation
- MMode
- Constructive Type Classes in Isabelle
- Local Theory Specifications in Isabelle/Isar
- Merging Procedural and Declarative Proof
- SWT
- KAT-ML: an interactive theorem prover for Kleene algebra with tests
- PairingHeap
This page was built for software: Isabelle/Isar
