Eisbach: a proof method language for Isabelle
From MaRDI portal
Recommendations
- An Isabelle proof method language
- A proof strategy language and proof script generation for Isabelle/HOL
- Structured Induction Proofs in Isabelle/Isar
- Isabelle's metalogic: formalization and proof checker
- Isabelle as document-oriented proof assistant
- The Isabelle/Naproche natural language proof assistant
- Logic Based Program Synthesis and Transformation
- Equational reasoning in Isabelle
- Isabelle/HOL. A proof assistant for higher-order logic
- A formalization and proof checker for Isabelle's metalogic
Cites work
- A formalized hierarchy of probabilistic system types. Proof pearl
- An introduction to small scale reflection in Coq
- An Isabelle proof method language
- Challenges and experiences in managing large-scale proofs
- Edinburgh LCF. A mechanized logic of computation
- How to make ad hoc proof automation less ad hoc
- scientific article; zbMATH DE number 1696760 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Locales: a module system for mathematical theories
- Mtac: a monad for typed tactic programming in Coq
- Noninterference for operating system kernels
- Secure Microkernels, State Monads and Scalable Refinement
- Types for Proofs and Programs
Cited in
(14)- TacticToe: learning to prove with tactics
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Parameterized synthesis for fragments of first-order logic over data words
- From LCF to Isabelle/HOL
- A proof strategy language and proof script generation for Isabelle/HOL
- An Isabelle proof method language
- Isabelle/jEdit – A Prover IDE within the PIDE Framework
- Beyond notations: hygienic macro expansion for theorem proving languages
- Highly automated formal proofs over memory usage of assembly code
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- Verifying feedforward neural networks for classification in Isabelle/HOL
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- A verified durable transactional mutex lock for persistent x86-TSO
- Pattern-based approach to automation of deductive verification of process-oriented programs: patterns, lemmas and algorithms
Describes a project that uses
Uses Software
This page was built for publication: Eisbach: a proof method language for Isabelle
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q287365)
