Basis Research Institute
Popular repositories Loading
-
ship-your-interpreter
ship-your-interpreter PublicLean 4 + the Sail-generated RISC-V ISA model prove, CompCert-style, that an inductive WHILE semantics abstracts a real interpreter binary — zero sorries, zero axioms
Repositories
- ship-your-lua Public
Verifying Lua 5.4 on bare-metal RV64 against a formal semantics, on the Sail RISC-V model, in Lean 4 + iris-lean
- ship-your-ocaml Public
Verifying OCaml's bootstrap compiler: bare-metal ocamlrun on the Sail RISC-V model, ZINC bytecode semantics, Lean 4 + iris-lean (plan, validation, scaffold)
- ship-your-interpreter Public
Lean 4 + the Sail-generated RISC-V ISA model prove, CompCert-style, that an inductive WHILE semantics abstracts a real interpreter binary — zero sorries, zero axioms
- dynestyx Public
Probabilistic programming for dynamical systems! Supports models with NumPyro, deterministic & stochastic systems, discrete- and continuous-time systems, and more!
- predicators Public Forked from Learning-and-Intelligent-Systems/predicators
Learning for effective and efficient bilevel planning
- toydb Public Forked from erikgrinaker/toydb
Distributed SQL database in Rust, written as an educational project
- vismatch Public Forked from gmberton/vismatch
Wrapper of 50+ image matching models with a unified interface
People
This organization has no public members. You must be a member to see who’s a part of this organization.
Top languages
Loading…
Most used topics
Loading…