Joomy Korkut

A plugin to type Unicode chars in Vim, using their LaTeX names.

A structure editor for a simple functional programming language, with Vim-like shortcuts and commands.

Turkish translation of Learn Haskell Fast and Hard by Yann Esposito.

a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features

Quick starter kit for Vim beginners.

joke page until I decide what to do with this domain name

Ottoman Divan poetry vezin checker in Haskell!

A classical propositional theorem prover in Haskell, using Wang's Algorithm.

A rule-based machine translation system from Ottoman Turkish to Modern Turkish.

Terminal based virtual piano in Haskell, with ncurses and Euterpea

Vim plugin to use emres/turkish-deasciifier

A Pacman implementation in Rocq, extracted to C++ via Crane.

using Data and Typeable to get a direct reflection system for free, when we're implementing a toy language in Haskell

Fuzzy string search in Haskell

Turkish NLP library in Haskell.

Simple terminal string styling in Haskell.

No description.

A Haskell implementation of distributed hash tables with two-phase commit.

Compilation of modal logic based functional language ML5 to JavaScript.

Documents (TeX, slides, poster etc.) for my master's thesis, titled "Edit-Time Tactics in Idris", and the TyDe '18 paper, titled "Extensible Type-Directed Editing"

A Minesweeper implementation in Rocq, extracted to C++ via Crane.

Simple microKanren implementation in Idris.

Documents (TeX, slides etc.) and code for the editor side metaprogramming in Coq.

A pseudo-Prolog that tries to answer queries by building the least Herbrand model.

Scraper for Twitter embedded timelines.

Haskell port of Deniz Yuret's Turkish deasciifier.

TeX files of my thesis

A formalization of the Calculus of Constructions

A tool for me to run a shell script between switching windows/apps on a Mac.

my PhD dissertation: Foreign Function Verification Through Metaprogramming

Sample code demonstrating features of typed Template Haskell.

A Reversi implementation in Rocq, extracted to C++ via Crane.

Turkish makam music tab player web app, with frets with decimals for microtones.

Hakyll blog source files.

my vim settings / plugins

Class project for COS561 with Prof. Jennifer Rexford: a Chrome app that calculates the optimal number of TCP parallel connections for maximum performance and loads in parallel.

A Dependently Typed Functional Programming Language

Simple Haskell bindings for Foma.

Civilization-like game in Haskell.

Verifying edit distance properties in Rocq.

commentary.vim: comment stuff out

The CompCert formally-verified C compiler

A rudimentary Vim clone in Coq, with CertiCoq and ncurses.

A CYK-parser for context-tree grammars.

Henk 2000

Simple matrix determinant calculator in different programming languages

Node.js replica of YouTube to MP3 web apps.

The network of programming languages

Generate Haskell code from a type

Personal website

SDL2 bindings in Rocq, for C++ extraction via Crane.

A separate repo with one example to test the performance of CertiCoq

A primitive set data structure for Coq, using `std::set` from C++.

Total Parser Combinators in Coq

Design ❤️ Code

A Verified Compiler for Gallina, Written in Gallina

A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.

No description.

A tiny dependent typechecker in Haskell, translated from @andrejbauer's OCaml

A library of Coq definitions, theorems, and tactics.

A gently curated list of companies using Haskell in industry

Reference type checker for the Lean theorem prover

A statically typed purely functional language with type-inferred recursive polymorphic variants.

Resurrecting Lennart Augustsson's implementation of Cayenne

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.

Presentation files.

Let GHC prove program equations for you

A Coq port of my paper Intrinsic Verification of a Regular Expression Matcher

Download and generate CSV files from Open Procurement tenders API.

Haskell library which makes word/tag clouds.

An image-processing library for Haskell.

An event management application built on Node.js

Asteroids... in Haskell!!

Text-based slides using vim and git.

A Haskell implementation of Peter Norvig's spelling corrector

An implementation of Martin Escardo's exhaustively searchable sets in Haskell.

A cleaned up version of ChartNew.js

JavaScript and vector graphics based space game.

Simple examples in MIPS Assembly.

Node.js app to scrape Wesleyan course catalog to output JSON.

Pie chart of languages of the repos that a GitHub user owns/starred/is watching.