Notes & Technical Writing
Here are my notes: short notes, mostly expository, about well-known or research problems, notes from self-studying mathematical texts, and lecture notes from lectures.
Expository Notes & Tutorials
An alternative proof of convergence for \( e^x \)
Proving that the exponential function converges using only the very basic facts about
infinite series.
[PDF]
Reynald Affeldt has formalized the proof in Coq, using the Mathematical Components Analysis library.
Introduction to topological K-theory
A brief introduction to the K-theory of topological spaces and its connection
with the K-theory of C*-algebras.
[PDF]
Formalized Mathematics
The Eckmann-Hilton Theorem
The higher homotopy groups are abelian. Mostly following the proof of Theorem 2.1.6 in
the
HoTT Book.
[GitHub]
Surveys
Securing Complex Software Systems Using Formal Verification and Specification
This was originally written as a course report for COMP 116, "Introduction to Computer
Security",
Fall 2017, Tufts University.
[PDF]
Project Reports
Formalizing the DFUDS Representation in Coq
Project report for CS 591K, "Foundations and Pragmatics of Dependently-Typed Systems",
Spring 2019,
Boston University.
(Note that the work reported is still very preliminary, and the approach outlined
might turn out not to be the most best approach.)
[PDF]
Exploring Corpora-Based Music Classification: Classifying Japanese Popular Music using
Lyrics
Project report for COMP 150WC, "Working with Corpora", Fall 2018, Tufts University.
[PDF]