Pinned Repositories
how-to-implement-dependent-type-theory
A tiny dependent typechecker in Haskell, translated from @andrejbauer's OCaml
preposterous
An implementation of the OutsideIn(X) constraint-based type inference engine "as seen in GHC"
rien
Predictable Haskell development environments with Cabal and Nix.
shorshe
freshly-fermented, dependently-typed mustard, with a substructural aftertaste
silica
optics for Haskell with the most amazing type errors you've seen
sound-and-complete
An implementation of the Dunfield-Krishnaswami "Sound and Complete" type-system
pebble
A toy symbolic algebra / calculus library in Haskell
pico
The Pico core language, and the Bake algorithm for elaborating Dependent Haskell into the former (WIP)
mrkgnao's Repositories
mrkgnao/pico
The Pico core language, and the Bake algorithm for elaborating Dependent Haskell into the former (WIP)
mrkgnao/system-dc
Strongly typed implementation of System DC, the core language for Dependent Haskell
mrkgnao/prosthetic-conscience
Towards a functional exocortex
mrkgnao/afterburner
incremental UI in Rust
mrkgnao/jeans
An experiment in using a theorem prover to find interesting new monads
mrkgnao/utt
The core type theory from the first chapter of Ulf Norell's (Agda) thesis
mrkgnao/mikrokosmos
Blog source, with Hakyll, type-of-html, and clay
mrkgnao/abseil
experiments in imperative incremental computation
mrkgnao/cube20rust
Rust port of Rokicki's cube20 representation and a human-method solver based on it
mrkgnao/cypherpunk-research
This repository is essentially for compiling information about Cypherpunks, the history of the movement, and the people/events of note.
mrkgnao/mythical-compiler
Notes for a compiler for an as-yet-nonexistent language
mrkgnao/ale
Check syntax in Vim asynchronously and fix files, with Language Server Protocol (LSP) support
mrkgnao/anki-editor
An Emacs package that helps you make Anki cards in Org-mode
mrkgnao/cabal-helper
Simple interface to some of Cabal's configuration state, used by ghc-mod. CI: https://gitlab.com/dxld/cabal-helper/pipelines
mrkgnao/doom.d
my doom.d
mrkgnao/eschatologist
mrkgnao/iced
A cross-platform GUI library for Rust, inspired by Elm
mrkgnao/idris2-vim
Vim mode for Idris 2
mrkgnao/interprocess
Portable interprocess communication (IPC) in Haskell
mrkgnao/llvm-hs-pretty
Pretty printer for LLVM AST to Textual IR
mrkgnao/miso-tutorial-app
GHCJS + Miso client, GHC + Servant server, Nix tying it all together
mrkgnao/mrkgnao.github.io
Free and open-source Jekyll theme
mrkgnao/notation
Collection of quotes on interesting notations & how they affect thought.
mrkgnao/periphero
wip
mrkgnao/phil2
Second iteration of my semi-serious toy compiler
mrkgnao/qtt
Quantitative Type Theory implementation
mrkgnao/rien-digest-example
Example usage of Rien with native dependencies
mrkgnao/smithay
A smithy for rusty wayland compositors
mrkgnao/sqlx
š§° The Rust SQL Toolkit. An async, pure Rust SQL crate featuring compile-time checked queries without a DSL.
mrkgnao/write-yourself-a-scheme-in-agda
Like "Write Yourself a Scheme in 48 Hours", but in Agda