Extensible Type-Directed Editing
with David Thrane Christiansen. TyDe ’18, 2018.
[preprint pdf]

Edit-Time Tactics in Idris
Master’s thesis, 2018. Advisor: Daniel R. Licata.
[pdf] [poster] [slides]

Thinking Outside the □: Verified Compilation of ML5 to JavaScript1
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. Unpublished draft, 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”.