Cited in
(15)- Size-based termination of higher-order rewriting
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- Paco
- wxHaskell
- Unbound
- HOLCF
- Stern-Brocot Tree
- Interactive programming in Agda -- objects and graphical user interfaces
- Unifiers as equivalences: proof-relevant unification of dependently typed data
- POPLMark reloaded: mechanizing proofs by logical relations
- Well-founded recursion with copatterns and sized types
- 2-Dimensional Directed Type Theory
- Monotone recursive types and recursive data representations in Cedille
- Flag-based big-step semantics
- Friends with benefits. Implementing corecursion in foundational proof assistants
This page was built for software: MiniAgda
