TYPES '07 talk by Ralph Matthes
The talk has been given at the TYPES meeting in Cividale del Friuli on May 3, 2007. Its abstract was:
Verification of the redecoration algorithm for triangular matrices
Ralph Matthes
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. Those families are now
fully supported in the newly released version 8.1 of Coq. Redecoration
of triangular matrices has a succint 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 Isabelle, giving insights
about the differences of both systems.
(joint work with Martin Strecker)
The overhead transparencies
Every page is a JPG file of approximately 1MB.
Ralph Matthes
