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.ECOOP.2022.12
URN: urn:nbn:de:0030-drops-162407
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16240/
Go to the corresponding LIPIcs Volume Portal

Rusu, Vlad ; Nowak, David

Defining Corecursive Functions in Coq Using Approximations

pdf-format:
LIPIcs-ECOOP-2022-12.pdf (0.8 MB)

Abstract

We present two methods for defining corecursive functions that go beyond what is accepted by the builtin corecursion mechanisms of the Coq proof assistant. This gain in expressiveness is obtained by using a combination of axioms from Coq’s standard library that, to our best knowledge, do not introduce inconsistencies but enable reasoning in standard mathematics. Both methods view corecursive functions as limits of sequences of approximations, and both are based on a property of productiveness that, intuitively, requires that for each input, an arbitrarily close approximation of the corresponding output is eventually obtained. The first method uses Coq’s builtin corecursive mechanisms in a non-standard way, while the second method uses none of the mechanisms but redefines them. Both methods are implemented in Coq and are illustrated with examples.

BibTeX - Entry

@InProceedings{rusu_et_al:LIPIcs.ECOOP.2022.12,
  author =	{Rusu, Vlad and Nowak, David},
  title =	{{Defining Corecursive Functions in Coq Using Approximations}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{12:1--12:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16240},
  URN =		{urn:nbn:de:0030-drops-162407},
  doi =		{10.4230/LIPIcs.ECOOP.2022.12},
  annote =	{Keywords: corecursive function, productiveness, approximation, Coq proof assistant}
}

Keywords: corecursive function, productiveness, approximation, Coq proof assistant
Collection: 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Issue Date: 2022
Date of publication: 23.06.2022
Supplementary Material: Software (ECOOP 2022 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.8.2.2

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