Verification of the Redecoration Algorithm for Triangular Matrices

Abstract

Triangular matrices with a dedicated type for the diagonal elements can be profitably represented by a nested datatype, i.e., a heterogeneous family of inductive datatypes. These families are fully supported since the version 8.1 of the Coq theorem proving environment, released in 2007. Redecoration of triangular matrices has a succinct implementation in this representation, thus giving the challenge of proving it correct. This has been achieved within Coq, using also induction with measures. An axiomatic approach allowed a verification in the Isabelle theorem prover, giving insights about the differences of both systems.

Online Copy

Available as PDF

BibTeX Entry

@InProceedings{matthes08:_verif_redec_algor_trian_matric,
  author = 	 {Ralph Matthes and Martin Strecker},
  title = 	 {Verification of the Redecoration Algorithm for Triangular Matrices},
  booktitle = 	 {Proc. TYPES 2007},
  pages =	 {125-141},
  year =	 2008,
  editor =	 {M. Miculan and I. Scagnetto and F. Honsell},
  volume =	 4941,
  series =	 {LNCS},
  publisher =	 {Springer}
}