Work & Research

Isabelle/HoTT

I created and continue to develop Isabelle/HoTT, an implementation of a homotopy type theory object logic for the interactive proof assistant Isabelle. It is currently expressive enough to support the formalization of large portions of the Homotopy Type Theory book.

Project home on GitHub: https://github.com/jaycech3n/Isabelle-HoTT

Targeted topic modeling

I was part of the team at Fraunhofer IAIS working on preprocessing and topic modeling of Twitter data to detect topics and trends in tweet corpora. I implemented probabilistic machine learning models, and processed and analyzed data using Python and Java. My work was applied in the European Union's E2mC Project for emergency and disaster management, as well as the CITYCoP system for community crime reporting.

Selected writing and presentations

An Implementation of Homotopy Type Theory in Isabelle/Pure, (2018). My Masters thesis, describing the theory behind an initial version of the Isabelle/HoTT implementation.

Computational Fact-Checking, (2017). A short survey report of various tasks and approaches in automated fact-checking.

Automated fact-checking, part 1 and part 2, (2017). Seminar talk presentation slides.

A pre-introduction to homotopy type theory, (2017). Notes for an introductory graduate talk given at the University of Bonn.

The Temperley-Lieb categories and skein modules, (2014). Honours thesis in category theory, quantum algebra, and low-dimensional topological invariants.