Isar
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Fractional generalization of the quantum Markovian master equation
- Proof assistants: history, ideas and future
- Isabelle
- mizar-items
- Sequoia
- Theorema
- Rapide
- Prosper
- IMP++
- Isabelle/HOL
- SecureUML
- MizarMode
- Isabelle/Isar
- IsaPlanner
- MAYA
- PVS
- A UTP semantic model for Orc language with execution status and fault handling
- MWB
- Metis
- CoSMed: a confidentiality-verified social media platform
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Formalization of the resolution calculus for first-order logic
- Omnibus
- distcc
- Mizar
- Foundational (co)datatypes and (co)recursion for higher-order logic
- IsaWin
- TAS
- Proof General
- Cabri-geometry
- Isabelle/ZF
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Netsoft
- A consistent foundation for Isabelle/HOL
- Flexary connectives in Mizar
- TeXmacs
- HOL
- HOL-OCL
- Matita
- Saoithin
- UTP2
- AEtnaNova
- PIDE
- Isabelle/jEdit
- HOL-Omega
- CeTA
- A comparison of Mizar and Isar
- MML
- Sledgehammer
- HOCL
- OMDoc
- Isabelle/PIDE
- ArgoCLP
- A generic and executable formalization of signature-based Gröbner basis algorithms
- LCF
- The Isabelle/Naproche natural language proof assistant
- GF
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- EAT
- jEdit
- Proof General Kit
- SmallCheck
- SAD
- ForTheL
- iJulienne
- NaCl
- Pcoq
- CtCoq
- PhoX
- PoplMark
- ProofWeb
- Relational characterisations of paths
- PRocH
- PROSPER
- SystemOnTPTP
- Bridging the gap between argumentation theory and the philosophy of mathematics
- From LCF to Isabelle/HOL
- Semantics of Mizar as an Isabelle object logic
- Poly/ML
- First steps towards a formalization of forcing
- Interactive verification of architectural design patterns in FACTum
- Using Isabelle/HOL to verify first-order relativity theory
- Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
- Formalizing complex plane geometry
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Formalizing provable anonymity in Isabelle/HOL
- From LTL to deterministic automata. A safraless compositional approach
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
- Flyspeck II: The basic linear programs
- Semantics, calculi, and analysis for object-oriented specifications
- Nominal Isabelle
- Automation for interactive proof: first prototype
- Referee
- Locales
- A graphical user interface for formal proofs in geometry
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
- Eisbach
- Master-equations for the study of decoherence
- Stochastic Schrödinger equation for a quantum oscillator with dissipation
- ConfiChair
This page was built for software: Isar
