Type Inference for ZFH

DOI10.1007/978-3-319-20615-8_6zbMath1417.68191OpenAlexW1772799650MaRDI QIDQ3453108

Phil Scott, Steven Obua, Jacques D. Fleuriot, David 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

Related Items (3)

Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ ProofScript: Proof Scripting for the Masses ⋮ Semantics of Mizar as an Isabelle object logic

Uses Software

• ML
• Isabelle/ZF
• kepler98
• ProofPeer

Cites Work

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

This page was built for publication: Type Inference for ZFH