I am Guilherme, a computer engineer fascinated with math, theorem provers, type theory, and logic. I like to prove theorems in Agda, Lean, Idris, and KeY. I am doing my PhD at Chalmers University, improving the SoldiKeY theorem prover. And after studying cubical type theory and theorem provers, I decided to create this blog to share my ideas and thoughts.
guilhermehas / cubical-1lab Goto Github PK
View Code? Open in Web Editor NEWThis project forked from plt-amy/1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
Home Page: https://cubical.1lab.dev
License: GNU Affero General Public License v3.0