License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.13
URN: urn:nbn:de:0030-drops-139083
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13908/
Go to the corresponding LIPIcs Volume Portal


Ciccone, Luca ; Dagnino, Francesco ; Zucca, Elena

Flexible Coinduction in Agda

pdf-format:
LIPIcs-ITP-2021-13.pdf (0.8 MB)


Abstract

We provide an Agda library for inference systems, also supporting their recent generalization allowing flexible coinduction, that is, interpretations which are neither inductive, nor purely coinductive. A specific inference system can be obtained as an instance by writing a set of meta-rules, in an Agda format which closely resembles the usual one. In this way, the user gets for free the related properties, notably the inductive and coinductive intepretation and the corresponding proof principles. Moreover, a significant modularity is achieved. Indeed, rather than being defined from scratch and with a built-in interpretation, an inference system can also be obtained by composition operators, such as union and restriction to a smaller universe, and its semantics can be modularly chosen as well. In particular, flexible coinduction is obtained by composing in a certain way the interpretations of two inference systems. We illustrate the use of the library by several examples. The most significant one is a big-step semantics for the λ-calculus, where flexible coinduction allows to obtain a special result (∞) for all and only the diverging computations, and the proof of equivalence with small-step semantics is carried out by relying on the proof principles offered by the library.

BibTeX - Entry

@InProceedings{ciccone_et_al:LIPIcs.ITP.2021.13,
  author =	{Ciccone, Luca and Dagnino, Francesco and Zucca, Elena},
  title =	{{Flexible Coinduction in Agda}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13908},
  URN =		{urn:nbn:de:0030-drops-139083},
  doi =		{10.4230/LIPIcs.ITP.2021.13},
  annote =	{Keywords: inference systems, induction, coinduction}
}

Keywords: inference systems, induction, coinduction
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: The complete code of the library with all the examples discussed in the paper is available at
Software (Source Code): https://github.com/LcicC/inference-systems-agda archived at: https://archive.softwareheritage.org/swh:1:dir:955d11416c46a1ee1b0b913f0bc5f30bf3de9e97


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI