1 Search Results for "Picard, Celia"

Verification of redecoration for infinite triangular matrices using coinduction

Authors: Ralph Matthes and Celia Picard

Published in: LIPIcs, Volume 19, 18th International Workshop on Types for Proofs and Programs (TYPES 2011)

Finite triangular matrices with a dedicated type for the diagonal elements can be profitably represented by a nested data type, i. e., a heterogeneous family of inductive data types, while infinite triangular matrices form an example of a nested coinductive type, which is a heterogeneous family of coinductive data types. Redecoration for infinite triangular matrices is taken up from previous work involving the first author, and it is shown that redecoration forms a comonad with respect to bisimilarity. The main result, however, is a validation of the original algorithm against a model based on infinite streams of infinite streams. The two formulations are even provably equivalent, and the second is identified as a special instance of the generic cobind operation resulting from the well-known comultiplication operation on streams that creates the stream of successive tails of a given stream. Thus, perhaps surprisingly, the verification of redecoration is easier for infinite triangular matrices than for their finite counterpart. All the results have been obtained and are fully formalized in the current version of the Coq theorem proving environment where these coinductive datatypes are fully supported since the version 8.1, released in 2007. Nonetheless, instead of displaying the Coq development, we have chosen to write the paper in standard mathematical and type-theoretic language. Thus, it should be accessible without any specific knowledge about Coq.

Cite as

Ralph Matthes and Celia Picard. Verification of redecoration for infinite triangular matrices using coinduction. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 55-69, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

  author =	{Matthes, Ralph and Picard, Celia},
  title =	{{Verification of redecoration for infinite triangular matrices using coinduction}},
  booktitle =	{18th International Workshop on Types for Proofs and Programs (TYPES 2011)},
  pages =	{55--69},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-49-1},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{19},
  editor =	{Danielsson, Nils Anders and Nordstr\"{o}m, Bengt},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2011.55},
  URN =		{urn:nbn:de:0030-drops-39001},
  doi =		{10.4230/LIPIcs.TYPES.2011.55},
  annote =	{Keywords: nested datatype, coinduction, theorem proving, Coq}
  • Refine by Author
  • 1 Matthes, Ralph
  • 1 Picard, Celia

  • Refine by Classification

  • Refine by Keyword
  • 1 Coq
  • 1 coinduction
  • 1 nested datatype
  • 1 theorem proving

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2013

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail