A Mechanized Translation from Higher-Order Logic to Set Theory

Abstract. In order to make existing formalizations available for settheoretic developments, we present an automated translation of theories from Isabelle/HOL to Isabelle/ZF. This covers all fundamental primitives, particularly type classes. The translation produces LCF-style theorems that are checked by Isabelle’s inference kernel. Type checking is replaced by explicit reasoning about set membership.

• Type: Conference
• Year: 2010
• Where: ITP
• Authors: Alexander Krauss, Andreas Schropp
• Keywords: Automated Translation, Fundamental Primitives, Isabelle’s Inference Kernel, ITP 2010, Mathematics