Thinking Outside the □: Verified Compilation of ML5 to JavaScript.1 Senior thesis, 2017. Advisor: Daniel R. Licata.
[pdf] [poster] [Agda code]

Intrinsic Verification of a Regular Expression Matcher. With Maksim Trifunovski and Daniel R. Licata. Submitted, 2016.
[pdf] [Agda code]

Other Writing

Turkish translation of Yann Esposito’s article Learn Haskell Fast and Hard

Notes for my automated theorem proving lectures, Spring 2016. Advisor: Olivier Hermant.


Hezarfen, a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features.
[Idris code]

distributed-hash-table, a Haskell implementation of distributed hash tables with two-phase commit.
[Haskell code]

WangsAlgorithm, a classical propositional theorem prover in Haskell, using Wang’s Algorithm.
[Haskell code]

herbrand-prolog, a pseudo-Prolog that tries to answer queries by building the least Herbrand model.
[Haskell code]

Divan.hs, Ottoman Divan poetry vezin checker in Haskell.
[Haskell code]

  1. Read the symbol □ as “box”.