Seminar

Wednesday, April 14th, 2021, 16:30, on Zoom.

Gianluca Amato (Chieti-Pescara)
Universal Algebra in UniMath (joint work with Marco Maggesi and Cosimo Perini Brogi)

Abstract:

In this talk we will report on recent experiments in implementing the basic notions of universal algebra in the Unimath library. Unimath is a replacement of the standard library of the Coq proof assistant based on the univalent foundations of mathematics. Since the use of general higher order inductive types is forbidden in Unimath, a relevant part of this work has been the implementation of terms as lists of function symbols in such a way that the operations on terms are computable by the standard Coq evaluation mechanism.

More information can be found in the preprint.

The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster or Giulio Fellin.