Type inference for ZFH

DOI10.1007/978-3-319-20615-8_6MaRDI QIDQ3453108zbMATH OpenOpenAlexFDO

Authors Steven Obua, Phil Scott, Jacques D. Fleuriot, D. Aspinall

Publication date 20 November 2015

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

Full work available at URL https://www.pure.ed.ac.uk/ws/files/19974278/Obua_et_al_2015_Type_Inference_for_ZFH.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Axiomatics of classical set theory and its fragments (03E30)

Recommendations

• Type inference for set theory
• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• Type inference in mathematics
• scientific article; zbMATH DE number 3881858
• Richer types for \(Z\)

Cites work

• A theory of type polymorphism in programming
• Coercions in a polymorphic type system
• Partial and nested recursive function definitions in higher-order logic
• Set theory for verification. I: From foundations to functions
• Term Rewriting and All That
• Theorem Proving in Higher Order Logics

Cited in

(6)

• Enumerated types and type extensions for MiniZinc
• Semantics of Mizar as an Isabelle object logic
• Presentation and manipulation of Mizar properties in an Isabelle object logic
• ProofScript: proof scripting for the masses
• Type inference in mathematics
• Mechanized HOL reasoning in set theory

Describes a project that uses

Uses Software

• ML
• Isabelle/ZF
• kepler98
• ProofPeer

This page was built for publication: Type inference for ZFH

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