Comprehending Isabelle/HOL's consistency

Conference paper


Kunčar, O. and Popescu, A. 2017. Comprehending Isabelle/HOL's consistency. Yang, H. (ed.) ESOP 2017: 26th European Symposium on Programming (ESOP). Uppsala, Sweden 22 - 29 Apr 2017 Berlin, Heidelberg Springer. https://doi.org/10.1007/978-3-662-54434-1_27
TypeConference paper
TitleComprehending Isabelle/HOL's consistency
AuthorsKunčar, O. and Popescu, A.
Abstract

The proof assistant Isabelle/HOL is based on an extension of Higher-Order Logic (HOL) with ad hoc overloading of constants. It turns out that the interaction between the standard HOL type definitions and the Isabelle-specific ad hoc overloading is problematic for the logical consistency. In previous work, we have argued that standard HOL semantics is no longer appropriate for capturing this interaction, and have proved consistency using a nonstandard semantics. The use of an exotic semantics makes that proof hard to digest by the community. In this paper, we prove consistency by proof-theoretic means—following the healthy intuition of definitions as abbreviations, realized in HOLC, a logic that augments HOL with comprehension types. We hope that our new proof settles the Isabelle/HOL consistency problem once and for all. In addition, HOLC offers a framework for justifying the consistency of new deduction schemas that address practical user needs.

LanguageEnglish
ConferenceESOP 2017: 26th European Symposium on Programming (ESOP)
Proceedings TitleESOP 2017: Programming Languages and Systems
SeriesLecture Notes in Computer Science
EditorsYang, H.
ISSN0302-9743
Electronic1611-3349
ISBN
Paperback9783662544334
Electronic9783662544341
PublisherSpringer
Place of publicationBerlin, Heidelberg
Publication dates
Online10 Apr 2017
Print19 Mar 2017
Publication process dates
Deposited19 Jun 2017
Accepted01 Mar 2017
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-54434-1_27

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-662-54434-1_27
Web address (URL) of conference proceedingshttps://doi.org/10.1007/978-3-662-54434-1
Permalink -

https://repository.mdx.ac.uk/item/870vq

Download files


Accepted author manuscript
  • 19
    total views
  • 3
    total downloads
  • 4
    views this month
  • 1
    downloads this month

Export as