Universidad de La RiojaCampus Iberus    
 
 
Principal Correo-web Directorio Mapa web Contacto
Información para
Estudiantes
Foreign students
Antiguos alumnos
Empresas
Visitantes
PDI/PAS
Información sobre
Universidad de La Rioja
Estudios
Campus Virtual
Investigación
Escuela Máster y Doctorado
Facultades y Escuelas
Departamentos
Administración y Servicios
Biblioteca
Fundación de la UR
Dialnet
Portal de transparencia
Unidad de Igualdad
Sede electrónica
Actualidad
Noticias
Agenda
Congresos y jornadas
Nuevas plazas PDI/PAS
Perfil del contratante
Boletines y publicaciones
 
facebook Twitter You Tube Flickr
pinterest linkedin instagram
 
Dialnet
 
Sede Electrónica
Agenda

15 de noviembre de 2017
11:00 horas
Seminario Miriam Andrés
Complejo Científico Tecnológico

Staff Week. Linear Algebra In Isabelle/HOLL
The Perron-Frobenius Theorem in Isabelle/HOL-Transferring between Matrix-Representations

René Thiemann
University of Innsbruck

Matrix interpretations are widely used in automated complexity analysis. For these interpretations, certification boils down to determining the growth rate of A^n for a fixed non-negative real matrix A.

Since the direct approach to compute the growth rate of A via algebraic numbers is quite slow, in this work we formalize the Perron-Frobenius theorem: it permits us to avoid algebraic numbers, so that our new certification algorithm only has to perform simple arithmetic operations. To cover the theorem in its full extend, we further establish a connection between two different Isabelle/HOL libraries on matrices, which enables an easy exchange of theorems between both libraries.

Actividad relacionada
·Staff Week. Linear Algebra in Isabelle/HOL

Archivos relacionados
Díptico

Servicio de Comunicación
comunicacion@adm.unirioja.es

  Noviembre  2017  
lu
ma
mi
ju
vi
sa
do
1 2 3 4 5
6 7 8 9 10 11 12
13 14 15 16 17 18 19
20 21 22 23 24 25 26
27 28 29 30
Agenda deportiva

Agenda administrativa

Inscripciones abiertas

Sobre este web | © Universidad de La Rioja