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: http://dagstuhl.sunsite.rwth-aachen.de/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)

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 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Issue Date: 2022
Date of publication: 23.06.2022

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