Abstract
ZFH stands for Zermelo-Fraenkel set theory implemented in higher-order logic. It is a descendant of Agerholm’s and Gordon’s HOL-ST but does not allow the use of type variables nor the definition of new types. We first motivate why we are using ZFH for ProofPeer, the collaborative theorem proving system we are building. We then focus on the type inference algorithm we have developed for ZFH. In ZFH’s syntax, function application, written as juxtaposition, is overloaded to be either set-theoretic or higher-order. Our algorithm extends Hindley-Milner type inference to cope with this particular overloading of function application. We describe the algorithm, prove its correctness, and discuss why prior general approaches to type inference in the presence of coercions or overloading do not cover our particular case.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
ProofPeer. http://www.proofpeer.net
Obua, S., Fleuriot, J., Scott, P., Aspinall, D.: ProofPeer: Collaborative Theorem Proving. http://arxiv.org/abs/1404.6186
Hales, T., et al.: A formal proof of the Kepler conjecture. http://arxiv.org/abs/1501.02155
Homotopy Type Theory. http://homotopytypetheory.org/
Agerholm, S., Gordon, M.: Experiments with ZF set theory in HOL and Isabelle. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971. Springer, Heidelberg (1995)
Gordon, M.: Set theory, higher order logic or both? In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996)
Paulson, L.C.: Set theory for verification: I. from foundations to functions. J. Autom. Reasoning 11(3), 353–389 (1993). Springer
Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reasoning 44(4), 303–336 (2010). Springer
ProofPeer Root Theory. http://proofpeer.net/repository?root.thy
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)
Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348–375 (1978)
Traytel, D., Berghofer, S., Nipkow, T.: Extending hindley-milner type inference with coercive structural subtyping. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 89–104. Springer, Heidelberg (2011)
Luo, Z.: Coercions in a polymorphic type system. Math. Struct. Comput. Sci. 18(04), 729–751 (2008). Cambridge Journals
Odersky, M., Wadler, P., Wehr, M.: A second look at overloading. In: Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture. ACM (1995)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Obua, S., Fleuriot, J., Scott, P., Aspinall, D. (2015). Type Inference for ZFH. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds) Intelligent Computer Mathematics. CICM 2015. Lecture Notes in Computer Science(), vol 9150. Springer, Cham. https://doi.org/10.1007/978-3-319-20615-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-20615-8_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-20614-1
Online ISBN: 978-3-319-20615-8
eBook Packages: Computer ScienceComputer Science (R0)