Disjoint sums over type classes in HOL

DOI10.1007/3-540-48256-3_2MaRDI QIDQ4945199zbMATH OpenFDO

Authors Norbert Völker

Publication date 23 August 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_2

zbMATH Keywords

datatypesdisjoint sumshigher-order logicmonomorphic sum typepolymorphic type systemsum type

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Axioms and decidability for type isomorphism in the presence of sums
• Types and indiscernibles in finite models
• scientific article; zbMATH DE number 3843744
• scientific article; zbMATH DE number 713392
• Disjunctions of Horn theories and their cores
• Disjunctions of Horn theories and their cores
• Coherent and Strongly Discrete Rings in Type Theory
• Type classes and filters for mathematical analysis in Isabelle/HOL
• Counting partial types in simple theories
• scientific article; zbMATH DE number 3927222

Cited in

(1)

• scientific article; zbMATH DE number 713392 (Why is no real title available?)

This page was built for publication: Disjoint sums over type classes in HOL

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