License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.11
URN: urn:nbn:de:0030-drops-77155
URL: http://drops.dagstuhl.de/opus/volltexte/2017/7715/
Go to the corresponding LIPIcs Volume Portal


Blanchette, Jasmin Christian ; Fleury, Mathias ; Traytel, Dmitriy

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL

pdf-format:
LIPIcs-FSCD-2017-11.pdf (0.5 MB)


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: 21.08.2017


DROPS-Home | Fulltext Search | Imprint Published by LZI