lolli-extract
| Crates.io | lolli-extract |
| lib.rs | lolli-extract |
| version | 0.2.0 |
| created_at | 2025-12-04 04:34:29.841387+00 |
| updated_at | 2025-12-05 04:02:47.735086+00 |
| description | Term extraction for the Lolli linear logic workbench |
| homepage | https://github.com/ibrahimcesar/lolli |
| repository | https://github.com/ibrahimcesar/lolli |
| max_upload_size | |
| id | 1965850 |
| size | 36,100 |
Ibrahim Cesar (ibrahimcesar)
documentation
README
lolli-extract
Term extraction for the Lolli linear logic workbench.
Extracts computational content (lambda terms) from proofs via the Curry-Howard correspondence.
Curry-Howard Correspondence
| Logic | Term |
|---|---|
| A ⊗ B | Pair |
| A ⊸ B | Function |
| A & B | Lazy pair |
| A ⊕ B | Sum (Either) |
| !A | Copyable value |
Usage
use lolli_extract::Extractor;
let mut extractor = Extractor::new();
let term = extractor.extract(&proof);
let normalized = term.normalize();
Part of Lolli
This is part of the Lolli linear logic workbench.
License
MIT