Seminars for Pure Mathematics
Jan 19 2023 |
| Ettore Aldrovandi (FSU) |
| Computer based formalization of Group Theory and Categorical Algebra in Homotopy Type Theory |
| Algebra and its Applications |
| Time: 3:05 pm |
| Location: LOV 0105 |
I describe some work in progress in collaboration with Keri D’angelo (Cornell — CS) to formalize crossed modules of groups, hence groups, in Homotopy Type Theory using the Agda proof assistant. No... More |
Jan 26 2023 |
| Ettore Aldrovandi (FSU) |
| Computer based formalization of Group Theory and Categorical Algebra in Homotopy Type Theory (Part II) |
| Algebra and its Applications |
| Time: 3:05 pm |
| Location: 0102 LOV |
I describe some work in progress in collaboration with Keri D’angelo (Cornell — CS) to formalize crossed modules of groups, hence groups, in Homotopy Type Theory using the Agda proof assistant. No... More |