Status

This is an active miniproject. The abstract theory is completely formalized; at the time of writing the concrete theory has no sorried definitions but it does have some sorried proofs.

The dependency explorer needs JavaScript and its graph data.