Pinned Repositories
btree-gadt
Code from a talk given at YOW! Lambda Jam 2013
coq-fight-2017
Lemmas contributed to the 2017 FP-Syd Coq Fight
puzzle-parity-permutations
Schrödinger's hats: a puzzle about parities and permutations
spacemacs-coq
A simple spacemacs layer for Coq including Company-Coq and Proof General
ylj15-coq-pattern-match
Code from a talk given at YOW! Lambda Jam 2015
mbrcknl's Repositories
mbrcknl/btree-gadt
Code from a talk given at YOW! Lambda Jam 2013
mbrcknl/spacemacs-coq
A simple spacemacs layer for Coq including Company-Coq and Proof General
mbrcknl/coq-fight-2017
Lemmas contributed to the 2017 FP-Syd Coq Fight
mbrcknl/ylj15-coq-pattern-match
Code from a talk given at YOW! Lambda Jam 2015
mbrcknl/puzzle-parity-permutations
Schrödinger's hats: a puzzle about parities and permutations
mbrcknl/await-remote-artifacts
GitHub action to wait for named artifacts to become available in another workflow, and to optionally download them.
mbrcknl/seL4-nix
mbrcknl/autocorres-examples
Example proofs about C programs using AutoCorres
mbrcknl/caddy
Fast, multi-platform web server with automatic HTTPS
mbrcknl/caddy-docker
mbrcknl/caddy_dns_cloudflare
Caddy module: dns.providers.cloudflare
mbrcknl/caddy_yaml_adapter
A config adapter which can read YAML for Caddy 2
mbrcknl/cakeml
CakeML: A Verified Implementation of ML
mbrcknl/ci-actions
CI GitHub actions for the seL4 repositories
mbrcknl/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
mbrcknl/coq-fight-2016
Lemmas for the 2016 FP-Syd Coq Fight
mbrcknl/functional.cc
Unfinished experiments in simulating algebraic datatypes with pattern-matching in C++
mbrcknl/git-repo
repo - The Multiple Git Repository Tool - (mirror of https://gerrit.googlesource.com/git-repo)
mbrcknl/graph-refine
mbrcknl/HOL
Canonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
mbrcknl/jekyll-sitemap
Jekyll plugin to silently generate a sitemaps.org compliant sitemap for your Jekyll site
mbrcknl/l4v
seL4 specification and proofs
mbrcknl/linode_api4-python
Official Python bindings for the Linode API
mbrcknl/mobile-ios
COVIDSafe IOS app
mbrcknl/seL4
The seL4 microkernel
mbrcknl/seL4_tools
Basic tools for building seL4 projects
mbrcknl/xcaddy
Build Caddy with plugins