TY - GEN
T1 - Nested multisets, hereditary multisets, & syntactic ordinals in Isabelle/HOL
AU - Blanchette, Jasmin Christian
AU - Fleury, Mathias
AU - Traytel, Dmitriy
PY - 2017
Y1 - 2017
N2 - 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).
AB - 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).
KW - Multisets
KW - Ordinals
KW - Proof assistants
UR - https://www.scopus.com/pages/publications/85029593244
UR - https://www.scopus.com/pages/publications/85029593244#tab=citedBy
U2 - 10.4230/LIPIcs.FSCD.2017.11
DO - 10.4230/LIPIcs.FSCD.2017.11
M3 - Conference contribution
AN - SCOPUS:85029593244
T3 - Leibniz International Proceedings in Informatics (LIPIcs)
SP - 1
EP - 18
BT - 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
A2 - Miller, Dale
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
Y2 - 3 September 2017 through 9 September 2017
ER -