Isar
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Comprehending Isabelle/HOL’s Consistency
- The seventeen provers of the world. Foreword by Dana S. Scott..
- A hierarchy of semantics for non-deterministic term rewriting systems
- scientific article; zbMATH DE number 1927420 (Why is no real title available?)
- Verified lightweight bytecode verification
- Flyspeck II: The basic linear programs
- Liveness Reasoning with Isabelle/HOL
- Building Formal Method Tools in the Isabelle/Isar Framework
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- A graphical user interface for formal proofs in geometry
- Specifying properties of dynamic architectures using configuration traces
- Towards Formal Proof Script Refactoring
- Faster and more complete extended static checking for the Java modeling language
- scientific article; zbMATH DE number 2090314 (Why is no real title available?)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Balancing the load. Leveraging a semantics stack for systems verification
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- First steps towards a formalization of forcing
- \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
- A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$
- MathLang Translation to Isabelle Syntax
- A user interface for a mathematical system that allows ambiguous formulae
- Formal Proof: Reconciling Correctness and Understanding
- A synthesis of the procedural and declarative styles of interactive theorem proving
- A Brief Overview of Mizar
- Social processes, program verification and all that
- Interactive verification of architectural design patterns in FACTum
- Formalization of the resolution calculus for first-order logic
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- On definitions of constants and types in HOL
- Semi-intelligible Isar proofs from machine-generated proofs
- A generic and executable formalization of signature-based Gröbner basis algorithms
- The Isabelle Framework
- Merging Procedural and Declarative Proof
- Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Automated Improving of Proof Legibility in the Mizar System
- A proof-centric approach to mathematical assistants
- A tactic language for declarative proofs
- Supporting the formal verification of mathematical texts
- Mathematical Knowledge Management
- Extending MKM formats at the statement level
- Formal Proof of the Group Law for Edwards Elliptic Curves
- Logic-Free Reasoning in Isabelle/Isar
- A UTP semantic model for Orc language with execution status and fault handling
- Local Theory Specifications in Isabelle/Isar
- Translating Scala programs to Isabelle/HOL. System description
- Implementing Spi Calculus Using Nominal Techniques
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- A Modular Type Reconstruction Algorithm
- Tutorial to locales and locale interpretation
- Using Isabelle/HOL to verify first-order relativity theory
- Computer theorem proving in mathematics
- From informal to formal proofs in Euclidean geometry
- Master-equations for the study of decoherence
- scientific article; zbMATH DE number 5713654 (Why is no real title available?)
- Mathematical Knowledge Management
- Shortening of proof length is elusive for theorem provers
- Structured Induction Proofs in Isabelle/Isar
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- Restoring Natural Language as a Computerised Mathematics Input Method
- Barendregt’s Variable Convention in Rule Inductions
- Declarative Proof Translation (Short Paper)
- Stochastic Schrödinger equation for a quantum oscillator with dissipation
- Fractional generalization of the quantum Markovian master equation
- Structured derivations: a unified proof style for teaching mathematics
- scientific article; zbMATH DE number 1614683 (Why is no real title available?)
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
- Quantum non-Markovian stochastic equations
- Relational characterisations of paths
- Verified analysis of random binary tree structures
- Mathematical method and proof
- Isabelle
- Theorema
- Rapide
- Prosper
- IMP++
- Isabelle/HOL
- SecureUML
- MizarMode
- Isabelle/Isar
- IsaPlanner
- MAYA
- PVS
- MWB
- distcc
- Omnibus
- Mizar
- Cabri-geometry
- IsaWin
- Proof General
- Isabelle/ZF
- Netsoft
- TAS
- HOL
- TeXmacs
- HOL-OCL
- Matita
- AEtnaNova
This page was built for software: Isar
