Show simple item record

dc.contributor.author
Traytel, Dmitriy
dc.date.accessioned
2020-05-20T06:49:56Z
dc.date.available
2018-02-16T13:31:05Z
dc.date.available
2018-02-19T09:25:18Z
dc.date.available
2020-05-20T06:49:56Z
dc.date.issued
2017-09-19
dc.identifier.issn
1860-5974
dc.identifier.other
10.23638/LMCS-13(3:28)2017
en_US
dc.identifier.uri
http://hdl.handle.net/20.500.11850/241647
dc.identifier.doi
10.3929/ethz-b-000241647
dc.description.abstract
Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branching over the alphabet, has been used to obtain compact and elegant proofs of classic results in language theory. In this article, we study this representation in the Isabelle proof assistant. We define regular operations on infinite tries and prove the axioms of Kleene algebra for those operations. Thereby, we exercise corecursion and coinduction and confirm the coinductive view being profitable in formalizations, as it improves over the set-of-words view with respect to proof automation.
en_US
dc.format
application/pdf
en_US
dc.language.iso
en
en_US
dc.publisher
Technische Universität Braunschweig
en_US
dc.rights.uri
http://creativecommons.org/licenses/by-nd/4.0/
dc.subject
Computer Science
en_US
dc.subject
Logic in Computer Science,Computer Science
en_US
dc.subject
Programming Languages
en_US
dc.title
Formal Languages, Formally and Coinductively
en_US
dc.type
Journal Article
dc.rights.license
Creative Commons Attribution-NoDerivatives 4.0 International
ethz.journal.title
Logical Methods in Computer Science
ethz.journal.volume
13
en_US
ethz.journal.issue
3
en_US
ethz.journal.abbreviated
Log. methods comput. sci.
ethz.pages.start
28
en_US
ethz.size
22 p.
en_US
ethz.version.deposit
publishedVersion
en_US
ethz.identifier.wos
ethz.publication.place
Braunschweig
en_US
ethz.publication.status
published
en_US
ethz.date.deposited
2018-02-16T13:31:17Z
ethz.source
WOS
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2018-02-19T09:25:21Z
ethz.rosetta.lastUpdated
2020-05-20T06:50:05Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Formal%20Languages,%20Formally%20and%20Coinductively&rft.jtitle=Logical%20Methods%20in%20Computer%20Science&rft.date=2017-09-19&rft.volume=13&rft.issue=3&rft.spage=28&rft.issn=1860-5974&rft.au=Traytel,%20Dmitriy&rft.genre=article&
 Search print copy at ETH Library

Files in this item

Thumbnail

Publication type

Show simple item record