# Research

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

[Markdown]

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

[pdf]

# Projects

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]

Read the symbol â–ˇ as â€śboxâ€ť.â†©