Verification of redecoration for infinite triangular matrices using coinduction

DOI10.4230/LIPICS.TYPES.2011.55MaRDI QIDQ2957696zbMATH OpenFDO

Authors Ralph Matthes, Celia Picard

Publication date 27 January 2017

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2011.55

zbMATH Keywords

coinductionCoqnested datatypetheorem proving

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Verification of the Redecoration Algorithm for Triangular Matrices
• Terminal semantics for codata types in intensional Martin-Löf type theory
• An application of co-inductive types in Coq: verification of the alternating bit protocol
• Circular coinduction in Coq using bisimulation-up-to techniques
• A coinductive calculus of binary trees

Cited in

(1)

• Verification of the Redecoration Algorithm for Triangular Matrices

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Verification of redecoration for infinite triangular matrices using coinduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2957696)