Show simple item record

dc.contributor.author
Blanchette, Jasmin C.
dc.contributor.author
Fleury, Mathias
dc.contributor.author
Traytel, Dmitriy
dc.contributor.editor
Miller, Dale
dc.date.accessioned
2018-04-13T09:23:00Z
dc.date.available
2017-10-19T02:10:01Z
dc.date.available
2017-12-07T16:22:42Z
dc.date.available
2018-04-12T14:37:33Z
dc.date.available
2018-04-13T09:23:00Z
dc.date.issued
2017
dc.identifier.isbn
978-3-95977-047-7
en_US
dc.identifier.issn
1868-8969
dc.identifier.other
10.4230/LIPIcs.FSCD.2017.11
en_US
dc.identifier.uri
http://hdl.handle.net/20.500.11850/197713
dc.identifier.doi
10.3929/ethz-b-000197713
dc.description.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).
en_US
dc.language.iso
en
en_US
dc.publisher
Schloss Dagstuhl, Leibniz-Zentrum für Informatik
en_US
dc.rights.uri
http://creativecommons.org/licenses/by/3.0/
dc.subject
Multisets
en_US
dc.subject
ordinals
en_US
dc.subject
proof assistants
en_US
dc.title
Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL
en_US
dc.type
Conference Paper
dc.rights.license
Creative Commons Attribution 3.0 Unported
ethz.book.title
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
en_US
ethz.journal.title
Leibniz International Proceedings in Informatics
ethz.journal.volume
84
en_US
ethz.journal.abbreviated
Leibniz int. proc. inform.
ethz.pages.start
11
en_US
ethz.size
18 p.
en_US
ethz.version.deposit
publishedVersion
en_US
ethz.event
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
en_US
ethz.event.location
Oxford, United Kingdom
en_US
ethz.event.date
September 3–9, 2017
en_US
ethz.identifier.urn
urn:nbn:de:0030-drops-77155
ethz.identifier.scopus
ethz.publication.place
Dagstuhl
en_US
ethz.publication.status
published
en_US
ethz.date.deposited
2017-10-19T02:10:02Z
ethz.source
SCOPUS
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-12-07T16:22:49Z
ethz.rosetta.lastUpdated
2020-02-15T12:21:40Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Nested%20multisets,%20hereditary%20multisets,%20and%20syntactic%20ordinals%20in%20Isabelle/HOL&rft.jtitle=Leibniz%20International%20Proceedings%20in%20Informatics&rft.date=2017&rft.volume=84&rft.spage=11&rft.issn=1868-8969&rft.au=Blanchette,%20Jasmin%20C.&Fleury,%20Mathias&Traytel,%20Dmitriy&rft.isbn=978-3-95977-047-7&rft.genre=proceeding&rft_id=info:doi/978-3-95977-047-7&rft.btitle=2nd%20International%20Conference%20on%20Formal%20Structures%20for%20Computation%20and%20Deduction%20(FSCD%202017)
 Search via SFX

Files in this item

Thumbnail

Publication type

Show simple item record