Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.11
URN: urn:nbn:de:0030-drops-77155
URL: https://drops.dagstuhl.de/opus/volltexte/2017/7715/
Blanchette, Jasmin Christian ; Fleury, Mathias ; Traytel, Dmitriy
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
| pdf-format: |
|
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 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).
BibTeX - Entry
@InProceedings{blanchette_et_al:LIPIcs:2017:7715,
author = {Jasmin Christian Blanchette and Mathias Fleury and Dmitriy Traytel},
title = {{Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL}},
booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
pages = {11:1--11:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-047-7},
ISSN = {1868-8969},
year = {2017},
volume = {84},
editor = {Dale Miller},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7715},
URN = {urn:nbn:de:0030-drops-77155},
doi = {10.4230/LIPIcs.FSCD.2017.11},
annote = {Keywords: Multisets, ordinals, proof assistants}
}
| Keywords: | Multisets, ordinals, proof assistants | |
| Seminar: | 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) | |
| Issue date: | 2017 | |
| Date of publication: | 30.08.2017 |
