Madrid, Spain
Computer Science Engineering student at Complutense University of Madrid (UCM). I am interested in type theory and how it can be used to make programs fast and correct.
Formalization of Mathematical Logic and Theoretical Computer Science in the Cubical Agda theorem prover