Nested multisets, hereditary multisets, & syntactic ordinals in Isabelle/HOL

Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

We present a collection of formalized results about finite nested multisets, developed using the Isabelle/HOL proof assistant. The nested multiset order is a generalization of the multiset order that can be used to prove termination of processes. Hereditary multisets, a variant of nested multisets, offer a convenient representation of ordinals below ϵ0. In Isabelle/HOL, both nested and hereditary multisets can be comfortably defined as inductive datatypes. Our formal library also provides, somewhat nonstandardly, multisets with negative multiplicities and syntactic ordinals with negative coefficients. We present applications of the library to formalizations of Goodstein's theorem and the decidability of unary PCF (programming computable functions).

Original languageEnglish
Title of host publication2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
EditorsDale Miller
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume84
ISBN (Electronic)9783959770477
DOIs
Publication statusPublished - 1 Sep 2017
Event2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 - Oxford, United Kingdom
Duration: 3 Sep 20179 Sep 2017

Conference

Conference2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
CountryUnited Kingdom
CityOxford
Period3/09/179/09/17

Keywords

  • Multisets
  • Ordinals
  • Proof assistants

Fingerprint Dive into the research topics of 'Nested multisets, hereditary multisets, & syntactic ordinals in Isabelle/HOL'. Together they form a unique fingerprint.

  • Cite this

    Blanchette, J. C., Fleury, M., & Traytel, D. (2017). Nested multisets, hereditary multisets, & syntactic ordinals in Isabelle/HOL. In D. Miller (Ed.), 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 (Vol. 84). [11] Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2017.11