Assorted Notes and Writings
This is an archive of my various technical notes/writings/documents that are interesting or might become useful (to me, or perhaps to you wanderers on the Internet) sometime. All written in English, of course.
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 project proposal. It contains unpublished original work on:
- Defunctionalization of Quantitative Type Theory
- Design of a dependently typed assembly language
- Formalization of hereditary substitution for STLC