scientific article; zbMATH DE number 1424013

MaRDI QIDQ4945201zbMATH OpenFDO

Authors Thomas Santen

Publication date 23 March 2000

zbMATH Keywords

higher-order logicHOLIsabelleshallow embeddingisomorphisms between typed sets

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

Cited in

(1)

• Structuring theories with implicit morphisms

Describes a project that uses

Uses Software

• Isabelle/HOL
• 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 Q4945201)