Name
Abstract | ||
|---|---|---|
In order to make existing formalizations available for set-theoretic 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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-14052-5_23 | ITP |
Keywords | Field | DocType |
fundamental primitive,type class,type checking,explicit reasoning,set membership,higher-order logic,inference kernel,set-theoretic development,automated translation,mechanized translation,lcf-style theorem,higher order logic,set theory | Kernel (linear algebra),HOL,Set theory,Discrete mathematics,Type checking,Computer science,Inference,Algorithm,Type variable,Higher-order logic | Conference |
Volume | ISSN | ISBN |
6172 | 0302-9743 | 3-642-14051-3 |
Citations | PageRank | References |
11 | 0.64 | 16 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexander Krauss | 1 | 215 | 11.99 |
| Andreas Schropp | 2 | 16 | 1.07 |