The Power of Pi
Nicolas Oury and Wouter Swierstra
The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008)
Victoria, British Columbia, Canada, September 22-24, 2008
This paper exhibits the power of programming with dependent types by dint of embedding three domain-specific languages: Cryptol, a language for cryptographic protocols; a small data description language; and relational algebra. Each example demonstrates particular design patterns inherent to dependently-typed programming. Documenting these techniques paves the way for further research in domain-specific embedded type systems.
Conference Manager (V2.54.6)