Add parallelism - Githubissues

jonsterling / agda-calf

A cost-aware logical framework, embedded in Agda.

https://jonsterling.github.io/agda-calf/

Apache License 2.0

55 stars 2 forks source link

Closed HarrisonGrodin closed 3 years ago

HarrisonGrodin commented 3 years ago

[x] Add infrastructure
- [X] Define ParCostMonoid structure
- [X] Add lazy products
- [x] Update cost infrastructure (upper bounds, etc.)
- [x] Always use additive structure
- [x] Support refinement lemmas
[x] Exp2 example
- [X] Write code
- [x] Prove upper bounds
- [x] Prove extensional equivalence

kaonn commented 3 years ago

lgtm!