-
-
-
type.systems Public
joke page until I decide what to do with this domain name
-
mcqc Public
Forked from mit-pdos/mcqcA Gallina compiler with C++17 as an intermediate representation
Haskell MIT License UpdatedMar 8, 2025 -
dissertation Public
my PhD dissertation: Foreign Function Verification Through Metaprogramming
-
CompCert Public
Forked from AbsInt/CompCertThe CompCert formally-verified C compiler
-
vim-in-coq Public
A rudimentary Vim clone in Coq, with CertiCoq and ncurses.
-
latex-unicoder.vim Public
A plugin to type Unicode chars in Vim, using their LaTeX names.
-
-
cyk-parser Public
A CYK-parser for context-tree grammars.
-
dilim Public
A structure editor for a simple functional programming language, with Vim-like shortcuts and commands.
-
certicoq-sha Public
A separate repo with one example to test the performance of CertiCoq
C UpdatedDec 4, 2023 -
cpp-coq-ffi Public
A primitive set data structure for Coq, using `std::set` from C++.
C++ UpdatedNov 21, 2023 -
certicoq Public
Forked from CertiCoq/certicoqA Verified Compiler for Gallina, Written in Gallina
Coq MIT License UpdatedSep 13, 2023 -
-
utopia Public
Forked from concrete-utopia/utopiaDesign ❤️ Code
TypeScript MIT License UpdatedDec 9, 2022 -
CertiGraph Public
Forked from CertiGraph/CertiGraphA library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.
Coq MIT License UpdatedOct 6, 2022 -
petgraph-automata Public
Forked from flippers2652/dfa_generatorRust MIT License UpdatedAug 6, 2022 -
WindowWatcher Public
Forked from kyo-ago/Automatically-Move-Mouse-Pointer-To-Default-Button-in-a-dialog-box-for-macA tool for me to run a shell script between switching windows/apps on a Mac.
-
zor-yoldan-haskell Public
Turkish translation of Learn Haskell Fast and Hard by Yann Esposito.
-
Divan.hs Public
Ottoman Divan poetry vezin checker in Haskell!
-
dilacar Public
A rule-based machine translation system from Ottoman Turkish to Modern Turkish.
-
direct-reflection-for-free Public
using Data and Typeable to get a direct reflection system for free, when we're implementing a toy language in Haskell
-
metaprogrammable-editor Public
Documents (TeX, slides etc.) and code for the editor side metaprogramming in Coq.
-
WangsAlgorithm Public
A classical propositional theorem prover in Haskell, using Wang's Algorithm.
-
haskell-companies Public
Forked from erkmos/haskell-companiesA gently curated list of companies using Haskell in industry
The Unlicense UpdatedApr 29, 2019 -
regexp-agda Public
-
connection-booster Public
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.
-
how-to-implement-dependent-type-theory Public
Forked from evertedsphere/how-to-implement-dependent-type-theoryA tiny dependent typechecker in Haskell, translated from @andrejbauer's OCaml
Haskell Other UpdatedJan 2, 2019 -
coq-ext-lib Public
Forked from rocq-community/coq-ext-libA library of Coq definitions, theorems, and tactics.
Coq Other UpdatedNov 14, 2018
{{ message }}