A Computer-Checked Library of Category Theory

Functors and F-Coalgebras

Bachelor thesis (2023)

Authors

P.H. Brandao de Araujo Electrical Engineering, Mathematics and Computer Science

Contributors

B.P. Ahrens Programming Languages - EEMCS (supervisor 1)
L.F.B. Escot Programming Languages - EEMCS (supervisor 2)
Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright: © 2023 Pedro Henrique Brandao de Araujo
Category theory Proof assistant Functional Programming Coalgebra
More Info
expand_more

Published Date

27-06-2023

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

This research project aims to develop a computer-checked library of category theory within the Lean proof assistant, with a specific emphasis on concepts and examples relevant to functional programming. Category theory offers a robust mathematical framework that allows for the abstraction and comprehension of concepts across diverse fields, including computer science. Additionally, the project will explore the application of final coalgebras, particularly in the context of understanding infinite data structures. By creating a formalized category theory library within Lean, our objective is to enhance our understanding of functional programming and programming language concepts. Moreover, we aim to facilitate the study of these topics by providing a comprehensible library and a rigorous foundation for program reasoning, thereby benefiting researchers and practitioners in the field.