AdrienChampion
Independent R&D Engineer in Lean 4 and Rust (and OCaml if I have to)
anzenlangLa Rochelle, France
Pinned Repositories
benchi
Benchmark easily with `benchi`
collChoSoWel
experimentalean4
Experimenting with lean4
fast_expr
Fast expressions.
hashconsing
A Rust hashconsing library.
hoice
A Horn Clause ICE engine.
rsmt2
A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
safe_index
Safe indexing in Rust.
safeIdx
Type-safe indexing library.
zdd
AdrienChampion's Repositories
AdrienChampion/hashconsing
A Rust hashconsing library.
AdrienChampion/collChoSoWel
AdrienChampion/safe_index
Safe indexing in Rust.
AdrienChampion/benchi
Benchmark easily with `benchi`
AdrienChampion/loadTerms.lean
Testing dynamic term loading in Lean 4.
AdrienChampion/safeIdx
Type-safe indexing library.
AdrienChampion/experimentalean4
Experimenting with lean4
AdrienChampion/hoice
A Horn Clause ICE engine.
AdrienChampion/lsmt2
Interact with SMT-LIB 2 compliant solvers in Lean 4
AdrienChampion/timelib
A date and time library for Lean 4
AdrienChampion/rsmt2
A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
AdrienChampion/erased-serde
Type-erased Serialize, Serializer and Deserializer traits
AdrienChampion/gayolGate
Information about my GitHub profile
AdrienChampion/implem
A small Rust library providing a helper macro for implementing common traits.
AdrienChampion/induction_for_dummies
Induction as a formal program verification technique for the uninitiated.
AdrienChampion/lean-smt
Tactics for discharging Lean goals into SMT solvers.
AdrienChampion/lean4
Lean 4 programming language and theorem prover
AdrienChampion/lean4-metaprogramming-book
AdrienChampion/mathlib4
Work in progress mathlib port for lean 4
AdrienChampion/matla
A manager for TLA+ projects.
AdrienChampion/mikino
A simple induction and BMC engine.
AdrienChampion/mikino_bin
A simple induction and BMC engine.
AdrienChampion/rust
Empowering everyone to build reliable and efficient software.
AdrienChampion/sat_micro_rust
AdrienChampion/std4
Standard Library for Lean 4
AdrienChampion/tagless.lean
Tagless parser library in Lean 4.
AdrienChampion/theorem_proving_in_lean4
Theorem Proving in Lean 4
AdrienChampion/tlaplus
TLC is an explicit state model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
AdrienChampion/ton-labs-assembler
AdrienChampion/ton-labs-types