The power of Pi

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.

• Type: Conference
• Year: 2008
• Where: ICFP
• Authors: Nicolas Oury, Wouter Swierstra
• Keywords: Data Description Language, Domain-specific Embedded Type, Domain-specific Languages, ICFP 2008, Programming Languages