Search Results

Documents authored by Nowak, David

Document
Artifact
DOI: 10.4230/DARTS.8.2.2
Defining Corecursive Functions in Coq Using Approximations (Artifact)

Authors: Vlad Rusu and David Nowak

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

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

Vlad Rusu and David Nowak. Defining Corecursive Functions in Coq Using Approximations (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/DARTS.8.2.2},
  URN =		{urn:nbn:de:0030-drops-162001},
  doi =		{10.4230/DARTS.8.2.2},
  annote =	{Keywords: corecursive function, productiveness, approximation, Coq proof assistant.}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.12
Defining Corecursive Functions in Coq Using Approximations

Authors: Vlad Rusu and David Nowak

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

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.
Cite as

Vlad Rusu and David Nowak. Defining Corecursive Functions in Coq Using Approximations. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 12:1-12:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ECOOP.2022.12},
  URN =		{urn:nbn:de:0030-drops-162407},
  doi =		{10.4230/LIPIcs.ECOOP.2022.12},
  annote =	{Keywords: corecursive function, productiveness, approximation, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.2
Extending Equational Monadic Reasoning with Monad Transformers

Authors: Reynald Affeldt and David Nowak

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a standard technique to combine monads. In this paper, we extend Monae, a Coq library for monadic equational reasoning, with monad transformers and we explain the benefits of this extension. Our starting point is the existing theory of modular monad transformers, which provides a uniform treatment of operations. Using this theory, we simplify the formalization of models in Monae and we propose an approach to support monadic equational reasoning in the presence of monad transformers. We also use Monae to revisit the lifting theorems of modular monad transformers by providing equational proofs and explaining how to patch a known bug using a non-standard use of Coq that combines impredicative polymorphism and parametricity.
Cite as

Reynald Affeldt and David Nowak. Extending Equational Monadic Reasoning with Monad Transformers. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.TYPES.2020.2,
  author =	{Affeldt, Reynald and Nowak, David},
  title =	{{Extending Equational Monadic Reasoning with Monad Transformers}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{2:1--2:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.2},
  URN =		{urn:nbn:de:0030-drops-138810},
  doi =		{10.4230/LIPIcs.TYPES.2020.2},
  annote =	{Keywords: monads, monad transformers, Coq, impredicativity, parametricity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact