Searched for: contributor%3A%22Ahrens%2C+B.P.+%28mentor%29%22
(1 - 14 of 14)
document
Greeve, Tiago (author)
This paper will give a formalisation of proofs, given in the paper "isomorphism is equality", in the proof assistant language Coq. The formalisations will be added to UniMath library. A library containing machine readable proofs in the mathematical field of Homotopy Type theory, a relatively new field which combines Homotopy Theory and Martin...
bachelor thesis 2023
document
van de Laar, Luuk (author)
This paper focuses on implementing and verifying the proofs presented in ``Finite Sets in Homotopy Type Theory" within the UniMath library. The UniMath library currently lacks support for higher inductive types, which are crucial for reasoning about finite sets in Homotopy Type Theory. This paper addresses that issue and introduces higher...
bachelor thesis 2023
document
Sarker, Pallabi Sree (author)
To address the challenge of the time-consuming nature of proofreading proofs, computer proof assistants—such as the Coq proof assistant—have been developed. The Univalent Mathematics project aims to formalise mathematics using the Coq proof assistant from a univalent perspective, which is based on homotopy type theory. <br/><br/>The Symmetry...
bachelor thesis 2023
document
Stanciu, Ciprian (author)
Existing implementations of category theory for proof assistants aim to be as generic as possible in order to be reusable and extensible, often at the expense of readability and clarity. We present a (partial) formalisation of category theory in the proof assistant Lean limited in purpose to explaining currying, intended to be faithful to the...
bachelor thesis 2023
document
Todorov, Rado (author)
Category theory is a branch of abstract mathematics that aims to give a high-level overview of relations between objects. Proof assistants are tools that aid in verifying the correctness of mathematical proofs. To reason about category theory using such assistants, fundamental notions have to be defined. Computer-checked libraries contain all...
bachelor thesis 2023
document
Farkas, Csanád (author)
Category Theory is a widely used field of Mathematics.<br/>Some concepts from it are often used in functional programming.<br/>This paper will focus on the Monad and a few implementations of it from Haskell.<br/>We will also present the computer-checked library we have written to help us in this task.
bachelor thesis 2023
document
Orav, Markus (author)
Category theory is a branch of mathematics that is used to abstract and generalize other mathematical concepts. Its core idea is to take the emphasis off the details of the elements of these concepts and put it on the relationships between them instead. The elements can then be characterized in terms of their relationships using various...
bachelor thesis 2023
document
Brandao de Araujo, Pedro Henrique (author)
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,...
bachelor thesis 2023
document
van Heiningen, Jeroen (author)
The goal of this paper is to formalize the Fundamental Group of the Circle within Coq and the Unimath library, as described in the paper by Mr Licata and Mr Shulman, and show it is isomorphic to Z. Fundamental groups are a powerful algebraic invariant for studying Homotopy theory, and provide deep, yet concise insights into the fundamental...
bachelor thesis 2023
document
Janssen, Boris (author)
The Statix meta-language has been developed in order to simplify the definition of static semantics in programming languages. A high-level static semantics definition of a language in Statix can be used to generate a type-checker, hence abstracting over the shared implementation details. Statix should be able to express the static semantics of...
master thesis 2023
document
Lixandru, Horia (author)
This paper is a literature survey on homotopy type theory, analyzing the formalization of sets within homotopy type theory. Set theory is embedded in homotopy type theory via h-sets, with all h-sets forming the type <b>Set</b>. This paper presents the properties of the type <b>Set </b>from a categorical perspective, comparing it with its set...
bachelor thesis 2022
document
Fincato de Loureiro, Giovanni (author)
This report explores the differences in implementations of homotopy type theory using different definitions of finite sets. The expressive ability of homotopy theory is explored when using the newly established definition and implementation of Kuratowski finite sets. This implementation is then compared to that when using the previously...
bachelor thesis 2022
document
Linssen, Anneke (author)
The incorporation of the univalence axiom into homotopy type theory has facilitated a new way of proving a basic result in algebraic topology: that the fundamental group of the circle is the integers (π1(S1) ≃ Z). This proof is formalised by Licata and Shulman. However, while the authors note that the univalence axiom is essential, it is not...
bachelor thesis 2022
document
Santana Trejo, Raul (author)
Type Theory enables mathematicians to perform proofs in a formal language that<br/>computers can understand. This enables computer-assisted proofs and the computerization of all mathematical knowledge. Homotopy Type Theory (HoTT) views types as topological spaces, unlocking new ways to understand and expand Type Theory. One of the most...
bachelor thesis 2022
Searched for: contributor%3A%22Ahrens%2C+B.P.+%28mentor%29%22
(1 - 14 of 14)