Programming Metamorphic Algorithms: An Experiment in Type-Driven Algorithm Design
Hsiang-Shang Ko

TL;DR
This paper explores how dependently typed programming can facilitate type-driven algorithm design by developing metamorphic algorithms within Agda, demonstrating the potential of type hints to guide correct-by-construction implementations.
Contribution
It demonstrates the use of dependently typed programming for designing metamorphic algorithms interactively, showcasing the potential of type-driven development to formalize and verify complex algorithms.
Findings
Successful development of Gibbons’s streaming algorithm in Agda
Formalization of Nakano’s jigsaw model with correctness guarantees
Illustration of type hints aiding algorithm design process
Abstract
In dependently typed programming, proofs of basic, structural properties can be embedded implicitly into programs and do not need to be written explicitly. Besides saving the effort of writing separate proofs, a most distinguishing and fascinating aspect of dependently typed programming is that it makes the idea of interactive type-driven development much more powerful, where expressive type information becomes useful hints that help the programmer to complete a program. There have not been many attempts at exploiting the full potential of the idea, though. As a departure from the usual properties dealt with in dependently typed programming, and as a demonstration that the idea of interactive type-driven development has more potential to be discovered, we conduct an experiment in ?type-driven algorithm design?: we develop algorithms from their specifications encoded in sophisticated…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
