Projects per year
Abstract / Description of output
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 language | English |
---|---|
Title of host publication | Intelligent Computer Mathematics |
Subtitle of host publication | International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings |
Publisher | Springer |
Pages | 87-101 |
Number of pages | 15 |
ISBN (Electronic) | 978-3-319-20615-8 |
ISBN (Print) | 978-3-319-20614-1 |
DOIs | |
Publication status | Published - 18 Jul 2015 |
Event | Conference on Intelligent Computer Mathematics - Washington, United States Duration: 13 Jul 2015 → 17 Jul 2015 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer International Publishing |
Volume | 9150 |
ISSN (Print) | 0302-9743 |
Conference
Conference | Conference on Intelligent Computer Mathematics |
---|---|
Country/Territory | United States |
City | Washington |
Period | 13/07/15 → 17/07/15 |
Fingerprint
Dive into the research topics of 'Type Inference for ZFH'. Together they form a unique fingerprint.Projects
- 1 Finished
Profiles
-
Jacques Fleuriot
- School of Informatics - Personal Chair of Artificial Intelligence
- Artificial Intelligence and its Applications Institute
- Data Science and Artificial Intelligence
Person: Academic: Research Active