Pinned Repositories
game-trees
Functions and proofs about game trees in Rocq, implemented as rose trees.
dilim
A structure editor for a simple functional programming language, with Vim-like shortcuts and commands.
Divan.hs
Ottoman Divan poetry vezin checker in Haskell!
hezarfen
a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features
latex-unicoder.vim
A plugin to type Unicode chars in Vim, using their LaTeX names.
type.systems
joke page until I decide what to do with this domain name
vim-starter
Quick starter kit for Vim beginners.
WangsAlgorithm
A classical propositional theorem prover in Haskell, using Wang's Algorithm.
zor-yoldan-haskell
Turkish translation of Learn Haskell Fast and Hard by Yann Esposito.
proof-tree-builder.github.io
A web-based graphical proof assistant for LK and Hoare logic.
joom's Repositories
joom/zor-yoldan-haskell
Turkish translation of Learn Haskell Fast and Hard by Yann Esposito.
joom/latex-unicoder.vim
A plugin to type Unicode chars in Vim, using their LaTeX names.
joom/type.systems
joke page until I decide what to do with this domain name
joom/Divan.hs
Ottoman Divan poetry vezin checker in Haskell!
joom/WangsAlgorithm
A classical propositional theorem prover in Haskell, using Wang's Algorithm.
joom/dilacar
A rule-based machine translation system from Ottoman Turkish to Modern Turkish.
joom/dilim
A structure editor for a simple functional programming language, with Vim-like shortcuts and commands.
joom/direct-reflection-for-free
using Data and Typeable to get a direct reflection system for free, when we're implementing a toy language in Haskell
joom/fuzzy
Fuzzy string search in Haskell
joom/regexp-agda
joom/metaprogrammable-editor
Documents (TeX, slides etc.) and code for the editor side metaprogramming in Coq.
joom/dissertation
my PhD dissertation: Foreign Function Verification Through Metaprogramming
joom/WindowWatcher
A tool for me to run a shell script between switching windows/apps on a Mac.
joom/blog
Hakyll blog source files.
joom/connection-booster
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.
joom/vimrc
my vim settings / plugins
joom/CompCert
The CompCert formally-verified C compiler
joom/cyk-parser
A CYK-parser for context-tree grammars.
joom/vim-in-coq
A rudimentary Vim clone in Coq, with CertiCoq and ncurses.
joom/certicoq
A Verified Compiler for Gallina, Written in Gallina
joom/certicoq-sha
A separate repo with one example to test the performance of CertiCoq
joom/CertiGraph
A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.
joom/coq-ext-lib
A library of Coq definitions, theorems, and tactics.
joom/cpp-coq-ffi
A primitive set data structure for Coq, using `std::set` from C++.
joom/haskell-companies
A gently curated list of companies using Haskell in industry
joom/how-to-implement-dependent-type-theory
A tiny dependent typechecker in Haskell, translated from @andrejbauer's OCaml
joom/joom.github.io
Personal website
joom/mcqc
A Gallina compiler with C++17 as an intermediate representation
joom/petgraph-automata
joom/utopia
Design ❤️ Code