Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL
Blanchette, Jasmin C.
- Conference Paper
Rights / licenseCreative Commons Attribution 3.0 Unported
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 epsilon-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). Show more
External linksSearch via SFX
Book title2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Journal / seriesLeibniz International Proceedings in Informatics
Pages / Article No.
PublisherSchloss Dagstuhl, Leibniz-Zentrum für Informatik
SubjectMultisets; ordinals; proof assistants
MoreShow all metadata