License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.8.2.2
URN: urn:nbn:de:0030-drops-162001
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16200/
Go back to Dagstuhl Artifacts Series


Rusu, Vlad ; Nowak, David

Defining Corecursive Functions in Coq Using Approximations (Artifact)

pdf-format:
DARTS-8-2-2.pdf (0.4 MB)
artifact-format:
DARTS-8-2-2-artifact-58285d6a9a89a270f39b6eed5d9c8eb8.zip (0.1 MB)

Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy.


Abstract

This is the formalization in the Coq proof assistant of the related conference article shown below.

BibTeX - Entry

@Article{rusu_et_al:DARTS.8.2.2,
  author =	{Rusu, Vlad and Nowak, David},
  title =	{{Defining Corecursive Functions in Coq Using Approximations (Artifact)}},
  pages =	{2:1--2:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Rusu, Vlad and Nowak, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16200},
  URN =		{urn:nbn:de:0030-drops-162001},
  doi =		{10.4230/DARTS.8.2.2},
  annote =	{Keywords: corecursive function, productiveness, approximation, Coq proof assistant.}
}

Keywords: corecursive function, productiveness, approximation, Coq proof assistant.
Collection: DARTS, Volume 8, Issue 1, Special Issue of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022)
Issue Date: 2022
Date of publication: 23.06.2022


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