Mica is a tool which automates differential testing for OCaml
modules. Mica parses an OCaml module signature and
automatically generates property-testing code specialized to
the interface, checking if two modules are observationally
equivalent.
Mechanized Type Soundness Proofs for the Hindley-Milner Type
System
Mechanized type soundness proofs for the Hindley-Milner (or
“Damas-Milner”) type system using the locally
nameless representation in Coq, along with the LNGen & Ott metatheory tools.
The proofs are for the non-syntax-directed version of the HM type
system, as presented in Peyton
Jones et al. (2007).
Discussed the theory of Differential Privacy (DP) and recent work
from the algorithm design & PL literature incorporating DP into
streaming algorithms.
Hladký et al. (2021)
proved a limit theorem for the no. of cliques in W-random graphs (an
inhomogeneous variant of Erdős-Rényi random graphs). In these slides, I
introduce the relevant background in graphon theory, provide a
high-level overview of Hladký et al.’s proofs & conduct numerical
simulations in Python verifying their results.
Proving Pólya’s Random Walk Theorem using Electric Network
Theory
In these slides, I discuss the applications of electric network
theory to random walks on integer lattices, focusing on Doyle
& Snell’s (1984) proof for Pólya’s Random Walk Theorem.
Slides for a talk I gave for CIS 6700 (Advanced
Topics in Programming Languages)
In these slides, I cover the Church & Scott encodings of various
datatypes in the untyped λ-calculus,
following the presentation in Pierce’s Types & Programming
Languages textbook.
Parsers in Haskell
Slides for a guest lecture for CIS 1940
(Introduction to Haskell)
In these slides, I cover monadic parser combinators (à la Parsec),
Haskell’s Applicative typeclass & testing parsers using
QuickCheck.
I also designed an assignment where students build a parser for
Lisp-style S-expressions using Applicative functors, and
test the correctness of their parser using round-trip properties in
QuickCheck.
A Unix-esque operating system implemented in C (~10k lines of
code)
I worked on the OS kernel, in particular implementing the scheduler
and handling signals/process statuses, as well as integrating the kernel
with the shell.
