The Computer Science Colloquium Series became a course in January 2019, offering students an hour credit to learn more about research topics in the Computer and Cyber Sciences from leading researchers in these fields. All presentations will be held online during the Spring 2021 semester. For more information about this course or if you are a guest outside of Augusta University wishing to tune in to a presentation, please contact Dr. Harley Eades.
In case you missed a presentation from the Fall 2020 colloquium series, you can view previous presentations here.
May 7, 2021: View "Excel Meets Lambda" by Andy Gordon.
May 14, 2021, 9-10 am, Dr. Assia Mahboubi, "Mathematical Structures in Dependent Type Theory".
*This presentation will not be recorded. Please RSVP to Dr. Eades to join via Zoom.
Abstract: The past decade has seen the advent of several large-scale digital libraries of formalised mathematics, written with the help of proof assistants. Most of these libraries are framed by hierarchies of formal algebraic structures. These structures play a similar role as Bourbaki’s mathematical structures, codifying the mathematical language used throughout the library, its vocabulary and its notational apparatus. The latter hierarchies can also be seen as a formal-proof-engineering device, which organises inheritance and sharing between various interfaces.
This talk will discuss the recent techniques proposed to design these hierarchies in proof assistants based on dependent type theory, the corresponding achievements, but also their pitfalls and limitations.
Dr. Mahboubi's presentation is the final presentation for the Spring 2021 semester. Thanks to all of you for participating and joining in these special presentations! Stay tuned for more information to come about future speakers for next semester.