lolli-codegen
| Crates.io | lolli-codegen |
| lib.rs | lolli-codegen |
| version | 0.2.0 |
| created_at | 2025-12-04 04:34:40.106899+00 |
| updated_at | 2025-12-05 04:02:57.199275+00 |
| description | Code generation for the Lolli linear logic workbench |
| homepage | https://github.com/ibrahimcesar/lolli |
| repository | https://github.com/ibrahimcesar/lolli |
| max_upload_size | |
| id | 1965851 |
| size | 26,499 |
Ibrahim Cesar (ibrahimcesar)
documentation
README
lolli-codegen
Code generation for the Lolli linear logic workbench.
Generates Rust code from linear logic proofs, enforcing resource invariants at compile time.
Type Mapping
| Linear Logic | Rust Type |
|---|---|
| A ⊗ B | (A, B) |
| A ⊸ B | impl FnOnce(A) -> B |
| A & B | With<A, B> |
| A ⊕ B | Either<A, B> |
| !A | Rc<A> |
| 1 | () |
| 0 | ! (never) |
Usage
use lolli_codegen::RustCodegen;
let mut codegen = RustCodegen::new();
let rust_code = codegen.generate_module(&proofs);
Part of Lolli
This is part of the Lolli linear logic workbench.
License
MIT