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
- scientific article; zbMATH DE number 1696760 (Why is no real title available?)
- A formalized hierarchy of probabilistic system types. Proof pearl
- An Isabelle proof method language
- An introduction to small scale reflection in Coq
- 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
- 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
(13)- Parameterized synthesis for fragments of first-order logic over data words
- Isabelle/jEdit – A Prover IDE within the PIDE Framework
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- An Isabelle proof method language
- A proof strategy language and proof script generation for Isabelle/HOL
- From LCF to Isabelle/HOL
- TacticToe: learning to prove with tactics
- Verifying feedforward neural networks for classification in Isabelle/HOL
- Highly automated formal proofs over memory usage of assembly code
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- scientific article; zbMATH DE number 7566057 (Why is no real title available?)
- A verified durable transactional mutex lock for persistent x86-TSO
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
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)
