Assorted Notes and Writings

Various technical notes/writings/documents that might be interesting, useful, or are simply nice-looking.

QTAL: A quantitatively and dependently typed assembly language
The first-year report submitted to Department of Computer Science as part of the PhD examination process, which is essentially a doctoral thesis proposal. It contains (currently) unpublished original work on:

• Defunctionalization of Quantitative Type Theory
• Design of a dependently typed assembly language
• Formalization of hereditary substitution for STLC

Rough notes on Glueing and NbE
Hand-written notes in accompany to Marcelo Fiore’s extended abstract Semantic analysis of normalization by evaluation for typed lambda calculus, with a few comments, explanations, and proofs. A modern version of the paper is also available.

Rough note on explicit substitution
Hand-written notes on lambda calculus with explicit substitution sturcture in the syntax, covering untyped, simply typed, and dependently typed situations.

Composition as audio signal processing
Master’s coursework essay on viewing music as signals, motif variations as signal transforms, and (musical) composition as (functional) composition (pun intended!).