up: Publications |
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} }
Last modified: Thu Jul 30 11:01:07 CEST 2009 |