Hi! I’m currently a PhD student in the Circuits and Systems group at Imperial College London, supervised by John Wickerson.

My research focuses on formalising the process of converting high-level programming language descriptions to correct hardware that is functionally equivalent to the input. This process is called high-level synthesis (HLS), and allows software to be turned into custom accelerators automatically, which can then be placed on field-programmable gate arrays (FPGAs). An implementation in the Coq theorem prover called Vericert can be found on Github.

I have also worked on random testing for FPGA synthesis tools. Verismith is a fuzzer that will randomly generate a Verilog design, pass it to the synthesis tool, and use an equivalence check to compare the output to the input. If these differ, the design is automatically reduced until the bug is located.



My personal dotfiles.


A formally verified high-level synthesis tool based on CompCert and written in Coq.


Simple zettelkasten mode for emacs.


Personal blog and website.


An implementation of the Calculus of Construction.


779d953 Add mmm-mode

a day ago via dotfiles

076b3d3 Add current changes

2 days ago via dotfiles

8809228 Add new files

2 days ago via dotfiles

7013532 Update and fix the transformation

5 days ago via vericert

d43f57e Add back changes to Abstr

7 days ago via vericert

3c33ec3 Add forest type

9 days ago via vericert

c0ef677 Merge remote-tracking branch 'origin/dev/scheduling' into dev/scheduling

10 days ago via vericert

2321c5e Add current changes

10 days ago via vericert

3f74c21 Merge remote-tracking branch 'origin/master'

15 days ago via dotfiles

68895af Update lemmas with new update function

15 days ago via vericert

21d2482 Add configuration to context

15 days ago via dotfiles

9eb18ec Prioritise org-zettelkasten

16 days ago via emacs-zettelkasten

5fa9480 Add new function to create custom ID

16 days ago via emacs-zettelkasten

13f415f Update copyright

16 days ago via emacs-zettelkasten

d139b6a Fix main proof

21 days ago via vericert
1 / 19