diff --git a/public/favicon.ico b/public/favicon.ico new file mode 100644 index 0000000..47e64c5 Binary files /dev/null and b/public/favicon.ico differ diff --git a/src/pages/about.mdx b/src/pages/about.mdx index a01008a..fc7ba4d 100644 --- a/src/pages/about.mdx +++ b/src/pages/about.mdx @@ -11,18 +11,30 @@ Hi there! :wave: -### Research +## Academic life -I'm learning about [cubical type theory][cubical]! -I'll probably write some blog posts as I learn more. - -For my master's thesis project, I'm investigating a mechanization of [spectral sequences] in [Cubical] [Agda]. -So far, I've been primarily working through the [homotopy type theory book][HoTTBook]. +I'm currently doing a thesis project for my master's program, involving the mechanization of [spectral sequences] using [cubical] [Agda]. +See some of my blog posts to follow along with my research! [spectral sequences]: https://en.wikipedia.org/wiki/Spectral_sequence [agda]: https://agda.readthedocs.io/en/latest/overview.html [hottbook]: https://homotopytypetheory.org/book/ +### Research projects + +- [**cubeviz**](https://mzhang.io/cubeviz/). A visualizer for cubical type theory that can assist with constructing `hcomp`s. +- [**type theory repo**](https://git.mzhang.io/michael/type-theory). The main repository for my Agda code for my research project. + +### Conferences and summer schools + +History of conferences and academic events I've attended. + +- [**ICFP 2024, PLMW workshop**](https://icfp24.sigplan.org/). Milan, Italy. +- **MURI 2024**. Pittsburgh, PA. +- [**Unimath 2024**](https://unimath.github.io/minneapolis2024/). Minneapolis, MN. +- [**OPLSS 2024**](https://www.cs.uoregon.edu/research/summerschool/summer24/). Boston, MA. +- [**Midwest PL Summit 2023**](https://mwpls2023.engin.umich.edu/). Ann Arbor, MI. + ### University Involvement I also love to participate in computing related student groups at the University