Ponente: Jesús Aransay (Universidad de La Rioja)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: martes 11 de octubre, 12:00

Nota: la charla se trata de una prueba de tiempo para la presentación del mismo titulo que tendrá lugar en el Seminario “Universality of Proofs” que se celebra en el Leibniz-Zentrum für Informatik (Schloss Dagstuhl).

Abstract: Data types admit different representations. The reasons to prioritise one or another range from efficiency to simplicity. Interactive theorem provers allow users to work with these representations and offer tools that ease their communication. These tools are required to preserve the formalism among the representations. In this talk we present some use cases in the proof assistant Isabelle/HOL, defining the scope of each of these tools and their possible scenarios.

Puedes encontrar las transparencias de la charla en este enlace.