scientific article; zbMATH DE number 1424013

zbMATH Open0942.03011MaRDI QIDQ4945201FDOQ4945201

Authors: Thomas Santen 

Publication date: 23 March 2000

Title of this publication is not available (Why is that?)

Recommendations

• Toward sharing libraries of mathematics between theorem provers
• scientific article; zbMATH DE number 1113859
• Shallow embedding of type theory is morally correct
• ``Everything is everything revisited: shapeshifting data types with isomorphisms and hylomorphisms
• An Interpretation of Isabelle/HOL in HOL Light

zbMATH Keywords

higher-order logicHOLIsabelleshallow embeddingisomorphisms between typed sets

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (1)

• Structuring theories with implicit morphisms

Uses Software

• Isabelle
• Isabelle/HOL

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 Q4945201)