Pinned Repositories
alternative-internet
A collection of interesting new networks and tech aiming at decentralisation (in some form).
hyperbible
The new revised international KJV-ASV-DRB-DBT-ERV-WBT-WEB-YET-AKJV-WNT version
knotation
Strange Loop 2015 talk: knot notation, enumeration, and drawing
linear-logic
An encoding of linear logic in Coq with minimal Sokoban and blocks world examples
notation
Collection of quotes on notation design & how it affects thought.
part-of-speech
a conversational interface for writing (with J. Juang) http://hypotext.co/part-of-speech
poemify
ever wanted to change water into wine? better: now you can change prose into poetry
syntax
Experiments with syntax and symbols
vst-crypto
SHA-256 and HMAC specs and lemmas (from VST)
k-qy's Repositories
k-qy/notation
Collection of quotes on notation design & how it affects thought.
k-qy/knotation
Strange Loop 2015 talk: knot notation, enumeration, and drawing
k-qy/linear-logic
An encoding of linear logic in Coq with minimal Sokoban and blocks world examples
k-qy/poemify
ever wanted to change water into wine? better: now you can change prose into poetry
k-qy/syntax
Experiments with syntax and symbols
k-qy/hyperbible
The new revised international KJV-ASV-DRB-DBT-ERV-WBT-WEB-YET-AKJV-WNT version
k-qy/alternative-internet
A collection of interesting new networks and tech aiming at decentralisation (in some form).
k-qy/part-of-speech
a conversational interface for writing (with J. Juang) http://hypotext.co/part-of-speech
k-qy/vst-crypto
SHA-256 and HMAC specs and lemmas (from VST)
k-qy/penrose
a system to automatically visualize mathematics
k-qy/tfjs-opt-tutorial
Quick tutorial on how to use tensorflow.js for optimization.
k-qy/fcf
Foundational Cryptography Framework for machine-checked proofs of cryptography, adding HMAC-DRBG spec and security proofs. Deprecated; see link for newest version
k-qy/HMAC-DRBG
modifying func_spec/rng/specs folder, original https://bitbucket.org/naphatkrit/rng
k-qy/magic
For the Diaconis card trick involving linear shift registers, calculates the 5 spectator cards.
k-qy/mern-crud
A simple records system using MongoDB, Express.js, React.js, and Node.js with real-time CRUD operations using Socket.io
k-qy/opencollective-frontend
Open Collective's Frontend. A React app powered by Next.js.
k-qy/thesis
TeX source and slides for my senior thesis on verifying HMAC-DRBG.
k-qy/vst-hmac
Formally proving equivalence between two specs of HMAC [obsolete -- see https://github.com/PrincetonUniversity/VST]
k-qy/women-in-programming-languages-research
Women in Programming Languages and Software Engineering Research