Jason Bell

This is a Coq development containing a machine-checked proof that the basic radix-2 Cooley-Tukey Fast Fourier Transform (FFT) algorithm correctly implements the Discrete Fourier Transform (DFT). I did this as a non-trivial exercise in certified programming, and to test my knowledge of Coq, that I had been building out of personal interest. This development uses the axiomatization of the real numbers from the standard library to implement basic operations on complex numbers and establish the ring structure and then uses that to implement the Fourier transforms. The proof is mainly structured into a series of lemmas and induction principles, before the main body of the proof, which is rather long due to the need to write out long equations at various stages.

This is a work in progress library of algorithms and other utility functions for competitive programming using the C++ programming language. I have been developing this library as I have been going through the problems from UVa Online Judge mentioned in the book "Competitive Programming 3" by Steven and Felix Halim. The library includes custom iterators/adapters, various tree structures, and a variety of algorithms useful for specific problems.

Tronpix is a decentralized application (Dapp) I built for the TRON blockchain, based on the famous Million Dollar Homepage website. The Dapp allows users to buy tokens that can be exchanged for 10x10 pixel plots on a large canvas, on which users can draw anything they want, and attach an associated link to a website URL of their choosing. Like any Dapp, it is driven by a smart contract, written in Solidity in this case, which controls the core functions of the Dapp, the rest of the Dapp being written in JavaScript, and relying on the TronLink browser extension being present to facilitate connections to the blockchain through TronWeb. The whole website was written from scratch in pure HTML, CSS, and JavaScript, including the functionality for drawing and inserting images on the canvas. Although the project didn’t attract many users, it was still a good exercise in understanding blockchain technologies.