Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Traytel, Dmitriy http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-59853
URL:

Formal Languages, Formally and Coinductively

pdf-format:


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 paper, 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.

BibTeX - Entry

@InProceedings{traytel:LIPIcs:2016:5985,
  author =	{Dmitriy Traytel},
  title =	{{Formal Languages, Formally and Coinductively}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5985},
  URN =		{urn:nbn:de:0030-drops-59853},
  doi =		{10.4230/LIPIcs.FSCD.2016.31},
  annote =	{Keywords: Formal languages, codatatypes, corecursion, coinduction, interactive theorem proving, Isabelle HOL}
}

Keywords: Formal languages, codatatypes, corecursion, coinduction, interactive theorem proving, Isabelle HOL
Seminar: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue date: 2016
Date of publication: 2016


DROPS-Home | Fulltext Search | Imprint Published by LZI