This is the Agda accompaniment for the paper Towards a Theory of Reach.
The agda implementation for the minimal language is in the Basic folder with components:
- Subs.agda - definition of substitution
- Exp.agda - definition of minimal language, small step semantics + reachability
- LazyNarrowing.agda - definiton of lazy narrowing reduction + forward reachability
- Sound.agda - soundness of lazy narrowing
- Complete.agda - completeness of lazy narrowing
- WellFound.agda - well foundness used in completeness, this is currently a well foundness specific to lazy narrowing and not as general as the well foundness stated in paper
The agda implementation for the language extended with application and lambda expressions is in the Func folder. The Exp, LazyNarrowing, Sound and Complete modules are extended.