scientific article; zbMATH DE number 1088221

MaRDI QIDQ4364537zbMATH OpenFDO

Authors Lawrence C. Paulson

Publication date 22 March 1999

zbMATH Keywords

cryptographic protocolsgeneric reasoninggeneric theorem prover Isabellelogic programmingproof toolsunification

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• The foundation of a generic theorem prover
• The Isabelle Framework
• Isabelle/HOL. A proof assistant for higher-order logic
• Set theory for verification. I: From foundations to functions

Cited in

(11)

• Set theory for verification. I: From foundations to functions
• The foundation of a generic theorem prover
• Equational reasoning in Isabelle
• Isabelle's metalogic: formalization and proof checker
• A formalization and proof checker for Isabelle's metalogic
• Structured formal development in Isabelle
• Building Formal Method Tools in the Isabelle/Isar Framework
• Support logic programming
• scientific article; zbMATH DE number 65526 (Why is no real title available?)
• scientific article; zbMATH DE number 1543300 (Why is no real title available?)
• Isabelle/HOL/GST: a formal proof environment for generalized set theories

Describes a project that uses

Uses Software

• Isabelle/HOL
• Isabelle/ZF
• Isabelle

This page was built for publication:

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