Isomorphisms -- a link between the shallow and the deep

DOI10.1007/3-540-48256-3_4MaRDI QIDQ4945201zbMATH OpenFDO

Authors Thomas Santen

Publication date 23 March 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48256-3_4

zbMATH Keywords

higher-order logicHOLIsabelleisomorphisms between typed setsshallow embedding

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Toward sharing libraries of mathematics between theorem provers
• Semantic foundations for embedding HOL in Nuprl
• 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: Isomorphisms -- a link between the shallow and the deep

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