Foundation.Cost

Definition Memoization Footprint via the Visited Monoid formalized

Definition Parallel Composition in CostM formalized

Definition Peak-Memory Cost via the Cells Monoid formalized

Definition The CostM Complexity Monad formalized

Example Worked Example: Balanced Parallel Sum Depth formalized

Example Worked Example: Constant-Space Boyer–Moore Majority formalized

Example Worked Example: Euclidean GCD Step Count formalized

Example Worked Example: Longest Common Subsequence DP Grid formalized

Example Worked Example: Memoized Fibonacci Footprint formalized

Example Worked Example: N-ary parList Depth Bound formalized

Example Worked Example: Quadratic Naive List Reversal formalized