Safety and conservativity of definitions in HOL and Isabelle/HOL
- Submitting institution
-
The University of Sheffield
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 7449
- Type
- D - Journal article
- DOI
-
10.1145/3158112
- Title of journal
- Proceedings of the ACM on Programming Languages
- Article number
- 24
- First page
- -
- Volume
- 2
- Issue
- POPL
- ISSN
- 2475-1421
- Open access status
- Compliant
- Month of publication
- December
- Year of publication
- 2017
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
1
- Research group(s)
-
F - Security of Advanced Systems
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- To boost user productivity, proof assistants often deviate from well-understood safe mechanisms for definition and reasoning. This can lead to proofs of False, potentially compromising libraries of results and impairing trust in formal verification. This paper solves an open problem in Higher-Order Logic (HOL) of relevance to HOL-based proof assistants, showing that HOL definitions are proof-theoretically safe in a strong sense. It is the culmination of a series of results by Popescu and Kuncar that started with discovering and fixing an inconsistency in Isabelle/HOL (ITP’16). A PhD at Uppsala University extends this work in novel directions (Arve Gegelbach, https://dblp.org/pid/229/4444.html).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -