30 marca 2017 10:00
Hans de Nivelle: PHOLI-calculus, a Partial Higher-Order Logic with Interfaces
The goal of PHOLI is to obtain a proof checker that I would like to use by myself, and in which I could check most of the proofs of my PhD thesis, and possibly other proofs. Until now, this goal was not obtained.
A proof checker should offer the following:
- Correctness
- Organisation (grouping by topic, generalization, minimization of dependencies)
- Possibility to Communicate Ideas.
I have tried out quite some proof checkers, and I didn't like any of them, for various reasons (undocumented, chaotic design, bad user interface, no features for structuring, lack of automation.)
I implemented a first version of PHOLI in 2013. It was indeed possible to check simple proofs, but its main goal of being user-friendly was not obtained, not even closely. Since then, I have redesigned the calculus, but not reimplemented it. I explain some of the main features of the calculus in the talk.
- Small, reusable contexts based on Interfaces: A small context is easier to understand then a big context. Because its parameters can be universally quantified, it is more likely that parts of it are reusable.
- Time stamps. Logical dependency does not dictate place in source files. Instead time stamps are used. This makes it possible to insert theorems and definitions at every place where it seems suitable.
- Partial Functions. Many functions are naturally partial, and any attempt to make them non-partial makes them uglier and less reusable.