Blaisorblade
Formal Methods Engineer at Bedrock Systems Inc. — Iris/Coq/λ calculus/Haskell/Agda
Bedrock Systems Inc.Berlin, Germany
Pinned Repositories
abt
Implementing Abstract Binding Trees (in Scala, ...)
Agda-playground
My Agda experiments
Anki-Android
Anki on Android
dot-iris
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
evalFromToAbsMachines
A Functional Correspondence between Evaluators and Abstract Machines
git-filter-branch-msgs
Update mentions of hashes in commits messages — for git-filter-branch. In Scala.
hoas-with-names
Represent functions using higher-order abstract syntax (HOAS) *using macros to save names*
minidot
Dependent Object Types (DOT), bottom up
Blaisorblade's Repositories
Blaisorblade/dot-iris
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization
Blaisorblade/secd-lambda-calculus
SECD for lambda calculus. Warning: Force-push on main allowed!
Blaisorblade/autosubst
Automation for de Bruijn syntax and substitution in Coq
Blaisorblade/autosubst2
Official repository of the Autosubst 2 project.
Blaisorblade/camlp5
Preprocessor / Pretty Printer for OCaml
Blaisorblade/cdf-mech-sem
Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
Blaisorblade/ceps
Coq Enhancement Proposals
Blaisorblade/cgraphs
Deadlock freedom in Iris
Blaisorblade/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.
Blaisorblade/coq-elpi
Coq plugin embedding elpi
Blaisorblade/coq-lens
Lenses in Coq
Blaisorblade/coq-plugin-template-atdgen
Template of Coq Plugin using the Dune build system, and showcasing some advanced features
Blaisorblade/coq-serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Blaisorblade/CoqCP
Blaisorblade/cubeval
high-performance cubical evaluation
Blaisorblade/docker-dot-iris
Docker images with dependencies for dot-iris
Blaisorblade/dune
A composable build system for OCaml.
Blaisorblade/elpi
Embeddable Lambda Prolog Interpreter
Blaisorblade/homebrew-cask
🍻 A CLI workflow for the administration of macOS applications distributed as binaries
Blaisorblade/homebrew-core
🍻 Default formulae for the missing package manager for macOS
Blaisorblade/homebrew-personal
Blaisorblade/my-ocaml-coq-benchs
Hacky scripts for comparing Coq on different OCaml versions (more professional and heavier ways exist!)
Blaisorblade/NOVA
NOVA Microhypervisor
Blaisorblade/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
Blaisorblade/opam-overlay
My Opam overlay
Blaisorblade/opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
Blaisorblade/pam_reattach
Reattach to the user's GUI session on macOS during authentication (for Touch ID support in tmux)
Blaisorblade/platform
Multi platform setup for Coq, Coq libraries and tools
Blaisorblade/ProjectEuler-Coq-test
Experiments from coq.zulipchat.com learning VST
Blaisorblade/vscoq
A Visual Studio Code extension for Coq [maintainer=@maximedenes]