Type-Theoretical Proofs for Commutative Ring Axioms of the Integers
July 30, 2022 | Section: Projects
Introduction This project was submitted as part of requirements for my MS. The objective was to constructively demonstrate the existence of the commutative Ring of Integers alongside proofs all its accompanying algebraic properties in a computer aided proof assistant called Agda. This research project was supervised by Professor Thorsten Altenkirch and I’m forever grateful for his time, expertise, and empathy towards my journey into this fantastic subject. I’m revising aspects of the thesis based on the feedback I received during the presentation.