scientific article; zbMATH DE number 7649970

DOI10.4230/LIPIcs.ITP.2019.21MaRDI QIDQ5875430

Fabian Immler, Jonas Rädle, Makarius Wenzel

Publication date: 3 February 2023

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Isabelle/HOLIsabellevirtualizationHOL4Isabelle/ML

Mathematics Subject Classification ID

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Isabelle/PIDE
• LCF
• Transfer
• Lifting
• Archive Formal Proofs
• OpenTheory

Cites Work

• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• Interaction with formal mathematical documents in Isabelle/PIDE
• NASA formal methods. Third international symposium, NFM 2011, Pasadena, CA, USA, April 18--20, 2011. Proceedings
• Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A Brief Overview of HOL4
• Scalable LCF-Style Proof Translation
• CakeML
• Importing HOL Light into Coq

This page was built for publication: