Documentos electrónicos accesibles: donde existe una necesidad, nace un derecho

 

Ponente: Eduardo Sáenz de Cabezón Irigaray (Universidad de La Rioja)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: lunes 27 de noviembre, 12:00

Resumen: La accesibilidad web y en documentos electrónicos es de imprescindible importancia para un cierto porcentaje de la población, importante para un porcentaje más amplio y conveniente para todos.

En esta charla abordaremos los principios fundamentales de la accesibilidad en el contexto del acceso a la información y daremos algunas recomendaciones sencillas para que nuestros documentos se acerquen a ser universalmente accesibles.

Puedes acceder a las transparencias de la charla a través del siguiente enlace.

Desarrollo de Cesens®: de la idea al mercado

 

Ponente: Carlos Acedo (Computer Engineer, Encore Lab)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: miércoles 22 de noviembre, 11:00

Resumen: Retrospectiva de los hitos y aspectos técnicos más relevantes de Cesens®, el sistema de monitorización de cultivos desarrollado por la empresa riojana Encore Lab, desde la concepción del proyecto hasta su lanzamiento al mercado. Se repasarán las tecnologías hardware y software en las que se basa el sistema, así como los principales problemas y soluciones que se dieron a lo largo del desarrollo.

An Isabelle/HOL formalisation of Green’s Theorem

 

Ponente: Mohammad Abdulaziz (Technische Universität München)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: viernes 17 de noviembre, 11:00

Resumen: We describe a formalisation of Green’s theorem, a fundamental result of multivariate calculus, in Isabelle/HOL. The theorem statement that we formalise is enough for most applications, especially in physics and engineering. An interesting aspect of our proof is that we neither formalise orientations nor region boundaries explicitly, with respect to the outwards-pointing normal vector. Instead we refer to homological equivalences between paths.

The slides of the talk can be found in the following link.

Semi-Automatic Asymptotics in Isabelle/HOL

 

Ponente: Manuel Eberl (Technische Universität München)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: jueves 16 de noviembre, 11:00

Resumen: Computer Algebra Systems can easily compute limits and asymptotic expansions of complicated real functions; interactive theorem provers, on the other hand, provide very little support for such problems and proving asymptotic properties of a function often involves long and tedious manual proofs. In this talk, I will present my work about bringing automation for real-valued asymptotics to Isabelle/HOL using multiseries expansions. This yields a procedure to automatically prove limits and ‘Big-O’ estimates of real-valued functions similarly to computer algebra systems like Mathematica and Maple – but while proving every step of the process correct.

The slides of the talk are available in the following link.

Recent development in Lean and its analysis

 

Ponente: Johannes Hölzl (Vrije Universiteit Amsterdam)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: jueves 16 de noviembre, 09:00

Resumen: I will present the current state of analysis in Lean 3. The formalization of the reals is based on the completion of uniform spaces, requiring a more extensive filter library. While the analysis in Lean is developed up to the Lebesgue measure, I mostly want to focus on topological spaces and measurable spaces, and compare their formalization with the one in Isabelle.

The slides of the talk are available from the following link.

Rigorous Numerics and Linear Algebra in Isabelle/HOL

 

Ponente: Fabian Immler (Technische Universität München)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: miércoles 15 de noviembre, 14:00

Resumen: In this talk, I will present which concepts and results from linear algebra are used in my verified rigorous numerical ODE solver. Instead of matrices I work with a type of bounded linear functions. Matrix operations are represented as (lists of) deeply embedded arithmetic expressions. I set up Lifting and Transfer to convert between the type class of Euclidean space and vectors or matrices.

The slides of the talk are available from the following link.

The Perron-Frobenius Theorem in Isabelle/HOL — Transferring between Matrix-Representations

Ponente: René Thiemann (University of Innsbruck)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: miércoles 15 de noviembre, 11:00

Resumen: 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.

The slides of the talk are available from the following link.