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 / logrel-mltt Goto Github PK
View Code? Open in Web Editor NEWThis project forked from mr-ohman/logrel-mltt
A Logical Relation for Martin-Löf Type Theory in Agda
License: MIT License