Representing Isabelle in LF

DOI10.4204/EPTCS.34.8MaRDI QIDQ6941737zbMATH OpenFDO

Authors Florian Rabe

Publication date 19 August 2025

Full work available at URL https://doi.org/10.4204/EPTCS.34.8

Mathematics Subject Classification ID

Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A formulation of the simple theory of types.
• A framework for defining logics
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Constructive Type Classes in Isabelle
• scientific article; zbMATH DE number 3819086 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 2003161 (Why is no real title available?)
• scientific article; zbMATH DE number 2238212 (Why is no real title available?)
• Institutions: abstract model theory for specification and programming
• Isabelle. A generic theorem prover
• Structural cut elimination. I: Intuitionistic and classical logic
• Structured theory presentations and logic representations
• The foundation of a generic theorem prover

This page was built for publication: Representing Isabelle in LF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6941737)