Type-Theoretic Proofs for the Commutative Ring Axioms of the Integers
July 30, 2022 | Section: Projects
Type-theoretic Proofs for the Ring Axioms of the Integers This research project constituted a partial conditional for my MS where I prove the existence of a certain mathematical construct called a Ring. I achieve this with the help of a computer-aided proof-assistant called Agda, a programming language based on intuitionist type theory, also called Martin-Löf type theory (MLTT). This research project was undertaken under Prof. Thorsten Altenkirch’s supervision, and I’m forever grateful for his time, expertise, and empathy towards my journey into this fantastic subject.