Pure Algebra
Pinned Loading
Repositories
- lean4-effect4 Public
- lean4-typescript Public
TypeScript as a target language for the pure-algebra Lean family: first-order syntax, deterministic rendering, identifier profile, host pins
- downstream Public
The pure-algebra Lean family as one tree: local copies of every package, built and tested together in dependency order (leanprover/downstream scripts)
- lean4-whatwg Public
WHATWG Streams Standard reified in Lean 4: spec-authoritative first-order model, relational semantics, EffHOL logic layer, checked TypeScript lowering
- lean4-effects Public
- effect4-tools Public
TypeScript-side tooling for the pure-algebra Lean family: host check harness, trace harness, AST export, Effect profile extractors
- lean4-nlp Public
- lean4-hash Public
Proved SHA-256/SHA-224 and SHA3-512 in Lean 4: bit-level FIPS specifications, native implementations, and machine-checked refinements between them; shared by lean4-WHATWG-streams and foldlab
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…