Safety and conservativity of definitions in HOL and Isabelle/HOL

Article

Kunčar, O. and Popescu, A. 2018. Safety and conservativity of definitions in HOL and Isabelle/HOL. Proceedings of the ACM on Programming Languages. 2, pp. 1-26. https://doi.org/10.1145/3158112
TypeArticle
TitleSafety and conservativity of definitions in HOL and Isabelle/HOL
AuthorsKunčar, O. and Popescu, A.
Abstract

Definitions are traditionally considered to be a safe mechanism for introducing concepts on top of a logic known to be consistent. In contrast to arbitrary axioms, definitions should in principle be treatable as a form of abbreviation, and thus compiled away from the theory without losing provability. In particular, definitions should form a conservative extension of the pure logic. These properties are crucial for modern interactive theorem provers, since they ensure the consistency of the logic, as well as a valid environment for total/certified functional programming.
We prove these properties, namely, safety and conservativity, for Higher-Order Logic (HOL), a logic implemented in several mainstream theorem provers and relied upon by thousands of users. Some unique features of HOL, such as the requirement to give non-emptiness proofs when defining new types and the impossibility to unfold type definitions, make the proof of these properties, and also the very formulation of safety, nontrivial.
Our study also factors in the essential variation of HOL definitions featured by Isabelle/HOL, a popular member of the HOL-based provers family. The current work improves on recent results which showed a weaker property, consistency of Isabelle/HOL’s definitions.

PublisherAssociation for Computing Machinery (ACM)
JournalProceedings of the ACM on Programming Languages
ISSN2475-1421
Publication dates
Online27 Dec 2017
Print06 Jan 2018
Publication process dates
Deposited19 Jan 2018
Accepted29 Oct 2017
Output statusPublished
Publisher's version
Accepted author manuscript
Copyright Statement

As a Gold Open Access journal, PACMPL is committed to making high-quality peer-reviewed scientific research in programming languages free of restrictions on both access and (re-)use. Through the generous support of ACM and SIGPLAN, all papers published in PACMPL are guaranteed permanent free online access to the definitive version in the ACM Digital Library.
Accepted version: Copyright © 2017 ACM. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in Proceedings of the ACM on Programming Languages, Volume 2 Issue POPL, January 2018, Article No. 24 , http://dx.doi.org/10.1145/3158112

Additional information

Proceedings of the ACM on Programming Languages, Volume 2 Issue POPL, January 2018. The published article is available on open access at: https://doi.org/10.1145/3158112

Digital Object Identifier (DOI)https://doi.org/10.1145/3158112
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/8768q

Log in to edit

Download files

Publisher's version
conserv_HOL_IsabelleHOL.pdf

Accepted author manuscript
conservDefThHOL_draft.pdf

  • 109
    total views
  • 39
    total downloads
  • 13
    views this month
  • 2
    downloads this month

Export as

Related outputs

CoCon: A conference management system with formally verified document confidentiality
Popescu, A., Lammich, P. and Hou, P. 2021. CoCon: A conference management system with formally verified document confidentiality. Journal of Automated Reasoning. 65 (2), pp. 321-356. https://doi.org/10.1007/s10817-020-09566-9
A formally verified abstract account of Gödel's incompleteness theorems
Popescu, A. and Traytel, D. 2019. A formally verified abstract account of Gödel's incompleteness theorems. Fontaine, P. (ed.) CADE 27 - 27th International Conference on Automated Deduction. Natel, Brazil 27 - 30 Aug 2019 Springer, Cham. pp. 442-461 https://doi.org/10.1007/978-3-030-29436-6_26
Bindings as bounded natural functors
Blanchette, J., Gheri, L., Popescu, A. and Traytel, D. 2019. Bindings as bounded natural functors. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Hotel Cascais Miragem, Cascais, Portugal 13 - 19 Jan 2019 Association for Computing Machinery (ACM). https://doi.org/10.1145/3290335
A formalized general theory of syntax with bindings
Gheri, L. and Popescu, A. 2017. A formalized general theory of syntax with bindings. 8th International Conference Interactive Theorem Proving. Brasilia, Brazil 26 - 29 Sep 2017 Cham Springer International Publishing. pp. 241-261 https://doi.org/10.1007/978-3-319-66107-0_16
Foundational (co)datatypes and (co)recursion for higher-order logic
Biendarra, J., Blanchette, J., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kunčar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R. and Traytel, D. 2017. Foundational (co)datatypes and (co)recursion for higher-order logic. 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017. Brasilia, Brazil 27 - 29 Sep 2017 Cham Springer International Publishing. pp. 3-21 https://doi.org/10.1007/978-3-319-66167-4_1
CoSMed: a confidentiality-verified social media platform
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2018. CoSMed: a confidentiality-verified social media platform. Journal of Automated Reasoning. 61 (1-4), pp. 113-119. https://doi.org/10.1007/s10817-017-9443-3
A formalized general theory of syntax with bindings
Gheri, L. and Popescu, A. 2017. A formalized general theory of syntax with bindings. 8th International Conference Interactive Theorem Proving (ITP). Brasília, Brazil 26 - 29 Sep 2017 Springer. pp. 241-261 https://doi.org/10.1007/978-3-319-66107-0_16
Foundational nonuniform (co)datatypes for higher-order logic
Blanchette, J., Meier, F., Popescu, A. and Traytel, D. 2017. Foundational nonuniform (co)datatypes for higher-order logic. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Reykjavik, Iceland 20 - 23 Jun 2017 IEEE. https://doi.org/10.1109/LICS.2017.8005071
Soundness and completeness proofs by coinductive methods
Blanchette, J., Popescu, A. and Traytel, D. 2017. Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning. 58 (1), pp. 149-179. https://doi.org/10.1007/s10817-016-9391-3
Friends with benefits: implementing corecursion in foundational proof assistants
Blanchette, J., Bouzy, A., Lochbihler, A., Popescu, A. and Traytel, D. 2017. Friends with benefits: implementing corecursion in foundational proof assistants. 26th European Symposium on Programming, ESOP 2017. Uppsala, Sweden 22 - 29 Apr 2017 Springer. https://doi.org/10.1007/978-3-662-54434-1_5
From types to sets by local type definitions in higher-order logic
Kunčar, O. and Popescu, A. 2016. From types to sets by local type definitions in higher-order logic. ITP 2016: 7th International Conference on Interactive Theorem Proving. Nancy, France 22 - 25 Aug 2016 Springer. https://doi.org/10.1007/978-3-319-43144-4_13
Comprehending Isabelle/HOL's consistency
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
CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2017. CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. 38th IEEE Symposium on Security and Privacy. San Jose, CA, USA 22 - 26 May 2017 Institute of Electrical and Electronics Engineers (IEEE). pp. 729-748 https://doi.org/10.1109/SP.2017.24
Encoding monomorphic and polymorphic types
Blanchette, J., Böhme, S., Popescu, A. and Smallbone, N. 2017. Encoding monomorphic and polymorphic types. Logical Methods in Computer Science. 12 (4). https://doi.org/10.2168/LMCS-12(4:13)2016
CoSMed: a confidentiality-verified social media platform
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2016. CoSMed: a confidentiality-verified social media platform. Blanchette, J.C. and Merz, S. (ed.) ITP 2016: 7th International Conference on Interactive Theorem Proving. Nancy, France 22 - 25 Aug 2016 Springer. pp. 87-106 https://doi.org/10.1007/978-3-319-43144-4_6
A consistent foundation for Isabelle/HOL
Kunčar, O. and Popescu, A. 2015. A consistent foundation for Isabelle/HOL. 6th conference on Interactive Theorem Proving (ITP). Nanjing, China 24 - 27 Aug 2015 Springer. pp. 234-252 https://doi.org/10.1007/978-3-319-22102-1_16
Weak bisimilarity coalgebraically
Popescu, A. 2009. Weak bisimilarity coalgebraically. Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009. Udine, Italy 07 - 10 Sep 2009 Springer. pp. 157-172
A semantic approach to interpolation
Popescu, A., Şerbănuţă, T. and Roşu, G. 2009. A semantic approach to interpolation. Theoretical Computer Science. 410 (12-13), pp. 1109-1128. https://doi.org/10.1016/j.tcs.2008.09.038
Incremental pattern-based coinduction for process algebra and its Isabelle formalization
Popescu, A. and Gunter, E. 2010. Incremental pattern-based coinduction for process algebra and its Isabelle formalization. Foundations of Software Science and Computation Structures (FOSSACS). Paphos, Cyprus 20 - 28 Mar 2010 Springer. pp. 109-127
More SPASS with Isabelle: superposition with hard sorts and configurable simplification
Blanchette, J., Popescu, A., Wand, D. and Weidenbach, C. 2012. More SPASS with Isabelle: superposition with hard sorts and configurable simplification. Interactive Theorem Proving (ITP), Third International Conference. Princeton, New Jersey, US 13 - 15 Aug 2012 Springer. pp. 345-360
Proving concurrent noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2012. Proving concurrent noninterference. 2nd International Conference on Certified Programs and Proofs (CPP 2012). Kyoto, Japan 13 - 15 Dec 2012 Springer. pp. 109-125
Formal verification of language-based concurrent noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2013. Formal verification of language-based concurrent noninterference. Journal of Formalized Reasoning. 6 (1), pp. 1-30. https://doi.org/10.6092/issn.1972-5787/3690
Noninterfering schedulers: when possibilistic noninterference implies probabilistic noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2013. Noninterfering schedulers: when possibilistic noninterference implies probabilistic noninterference. 5th Conference on Algebra and Coalgebra in Computer Science (CALCO). Warsaw, Poland 03 - 06 Sep 2013 Springer. pp. 236-252
Mechanizing the metatheory of sledgehammer
Blanchette, J. and Popescu, A. 2013. Mechanizing the metatheory of sledgehammer. 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013). Nancy, France 18 - 20 Sep 2013 Springer. pp. 245-260
Formalizing probabilistic noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2013. Formalizing probabilistic noninterference. 3rd International Conference on Certified Programs and Proofs (CPP 2013). Melbourne, VIC, Australia 11 - 13 Dec 2013 Springer International Publishing. pp. 259-275
Nonfree datatypes in Isabelle/HOL: animating a many-sorted metatheory
Schropp, A. and Popescu, A. 2013. Nonfree datatypes in Isabelle/HOL: animating a many-sorted metatheory. Certified Programs and Proofs (CPP). Melbourne, Australia 11 - 13 Dec 2013 Springer. pp. 114-130 https://doi.org/10.1007/978-3-319-03545-1_8
Witnessing (co)datatypes
Blanchette, J., Popescu, A. and Traytel, D. 2015. Witnessing (co)datatypes. 24th European Symposium on Programming (ESOP 2015). London, UK 11 - 18 Apr 2015 Springer. pp. 359-382
A conference management system with verified document confidentiality
Kanav, S., Lammich, P. and Popescu, A. 2014. A conference management system with verified document confidentiality. Biere, A. and Bloem, R. (ed.) 26th International Conference on Computer Aided Verification (CAV) 2014. Vienna, Austria 18 - 24 Jul 2014 Springer. pp. 167-183 https://doi.org/10.1007/978-3-319-08867-9_11
Unified classical logic completeness: a coinductive pearl
Blanchette, J., Popescu, A. and Traytel, D. 2014. Unified classical logic completeness: a coinductive pearl. 7th International Joint Conference on Automated Reasoning (IJCAR). Vienna, Austria 19 - 22 Jul 2014 Springer International Publishing. pp. 46-60
Making security type systems less ad hoc
Nipkow, T. and Popescu, A. 2014. Making security type systems less ad hoc. Information Technology. 56 (6), pp. 267-272. https://doi.org/10.1515/itit-2014-1060
Strong normalization for System F by HOAS on top of FOAS
Popescu, A., Gunter, E. and Osborn, C. 2010. Strong normalization for System F by HOAS on top of FOAS. 25th Annual IEEE Symposium on Logic in Computer Science (LICS). Edinburgh, United Kingdom 11 - 14 Jul 2010 Institute of Electrical and Electronics Engineers. pp. 31-40
Recursion principles for syntax with bindings and substitution
Popescu, A. and Gunter, E. 2011. Recursion principles for syntax with bindings and substitution. The 16th ACM SIGPLAN International Conference on Functional Programming. Tokyo 19 - 21 Sep 2011 Association for Computing Machinery (ACM). pp. 346-358
Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
Traytel, D., Popescu, A. and Blanchette, J. 2012. Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. 27th Annual IEEE Symposium on Logic in Computer Science (LICS). Dubrovnik, Croatia 25 - 28 Jun 2012 Institute of Electrical and Electronics Engineers (IEEE). pp. 596-605 https://doi.org/10.1109/LICS.2012.75
Truly modular (co)datatypes for Isabelle/HOL
Blanchette, J., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A. and Traytel, D. 2014. Truly modular (co)datatypes for Isabelle/HOL. 5th International Conference on Interactive Theorem Proving (ITP). Vienna, Austria 14 - 17 Jul 2014 Springer International Publishing. pp. 93-110
Cardinals in Isabelle/HOL
Blanchette, J., Popescu, A. and Taytel, D. 2014. Cardinals in Isabelle/HOL. 5th International Conference on Interactive Theorem Proving. Vienna, Austria 14 - 17 Jul 2014 Springer. pp. 111-127
Term-generic logic
Popescu, A. and Roşu, G. 2015. Term-generic logic. Theoretical Computer Science. 577, pp. 1-24. https://doi.org/10.1016/j.tcs.2015.01.047
Foundational extensible corecursion: a proof assistant perspective
Blanchette, J., Popescu, A. and Traytel, D. 2015. Foundational extensible corecursion: a proof assistant perspective. 20th ACM SIGPLAN International Conference on Functional Programming (ICFP). Vancouver, Canada 31 Aug - 02 Sep 2015 Association for Computing Machinery (ACM). pp. 192-204 https://doi.org/10.1145/2784731.2784732
Encoding monomorphic and polymorphic types
Blanchette, J., Böhme, S., Popescu, A. and Smallbone, N. 2013. Encoding monomorphic and polymorphic types. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Rome 16 - 24 Mar 2013 Springer. pp. 493-507