BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Combining Two Representations of Matrices for a Formalization of t
 he Perron-Frobenius Theorem - René Thiemann (University of Innsbruck)
DTSTART:20251127T170000Z
DTEND:20251127T180000Z
UID:TALK238729@talks.cam.ac.uk
CONTACT:Angeliki Koutsoukou-Argyraki
DESCRIPTION:Matrix interpretations are useful for automated complexity ana
 lysis of term\nrewrite systems. For checking the correct application of th
 ese interpretations\nin automatically generated proofs\, one needs a verif
 ied algorithm to determine\nthe asymptotic growth rate of A^n for a given 
 non-negative real matrix A.\n\nSince the direct approach to compute the gr
 owth rate of A via algebraic numbers\nis quite slow\, in our certifier CeT
 A we utilize a simple algorithm that does not\nrequire algebraic numbers. 
 Despite the simplicity of the algorithm\, its\nverification in Isabelle/HO
 L is technically interesting. For proving soundness\nof the algorithm\, we
  need to formalize the Perron-Frobenius theorem. And to\nachieve the latte
 r task\, we establish a connection between two different\nIsabelle/HOL lib
 raries on matrices\, that facilitates an easy exchange of\ntheorems betwee
 n both libraries.\n\n\n=== Hybrid talk ===\n\nJoin Zoom Meeting https://ca
 m-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1\n\nMeet
 ing ID: 898 5609 1954 Passcode: ITPtalk
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR