Type Inference for ZFH

Steven Obua, Jacques Fleuriot, Phil Scott, David Aspinall

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 over- loading do not cover our particular case.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publicationInternational Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings
PublisherSpringer International Publishing
Number of pages15
ISBN (Electronic)978-3-319-20615-8
ISBN (Print)978-3-319-20614-1
Publication statusPublished - 18 Jul 2015
EventConference on Intelligent Computer Mathematics - Washington, United States
Duration: 13 Jul 201517 Jul 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
ISSN (Print)0302-9743


ConferenceConference on Intelligent Computer Mathematics
Country/TerritoryUnited States


Dive into the research topics of 'Type Inference for ZFH'. Together they form a unique fingerprint.

Cite this