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