×

Type inference for ZFH. (English) Zbl 1417.68191

Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 87-101 (2015).
Summary: 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.
For the entire collection see [Zbl 1316.68015].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03E30 Axiomatics of classical set theory and its fragments
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] ProofPeer. http://www.proofpeer.net
[2] Obua, S., Fleuriot, J., Scott, P., Aspinall, D.: ProofPeer: Collaborative Theorem Proving. http://arxiv.org/abs/1404.6186
[3] Hales, T., et al.: A formal proof of the Kepler conjecture. http://arxiv.org/abs/1501.02155 · Zbl 1099.68725
[4] Homotopy Type Theory. http://homotopytypetheory.org/
[5] Agerholm, S.; Gordon, M.; Schubert, ET; Alves-Foss, J.; Windley, P., Experiments with ZF set theory in HOL and Isabelle, Higher Order Logic Theorem Proving and Its Applications (1995), Heidelberg: Springer, Heidelberg
[6] Gordon, M.; von Wright, J.; Harrison, J.; Grundy, J., Set theory, higher order logic or both?, Theorem Proving in Higher Order Logics (1996), Heidelberg: Springer, Heidelberg
[7] Paulson, LC, Set theory for verification: I. from foundations to functions, J. Autom. Reasoning, 11, 3, 353-389 (1993) · Zbl 0802.68128 · doi:10.1007/BF00881873
[8] Krauss, A., Partial and nested recursive function definitions in higher-order logic, J. Autom. Reasoning, 44, 4, 303-336 (2010) · Zbl 1214.68335 · doi:10.1007/s10817-009-9157-2
[9] ProofPeer Root Theory. http://proofpeer.net/repository?root.thy
[10] Baader, F.; Nipkow, T., Term Rewriting and All That (1999), Cambridge: Cambridge University Press, Cambridge · Zbl 0948.68098
[11] Milner, R., A theory of type polymorphism in programming, J. Comput. Syst. Sci., 17, 348-375 (1978) · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4
[12] Traytel, D.; Berghofer, S.; Nipkow, T.; Yang, H., Extending hindley-milner type inference with coercive structural subtyping, Programming Languages and Systems, 89-104 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-25318-8_10
[13] Luo, Z., Coercions in a polymorphic type system, Math. Struct. Comput. Sci., 18, 4, 729-751 (2008) · Zbl 1153.68010 · doi:10.1017/S0960129508006804
[14] 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)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.