%0 Conference Paper %1 Oury2008Power %A Oury, Nicolas %A Swierstra, Wouter %B Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08 %C New York %D 2008 %I ACM Press %K 03b15-higher-order-logic-type-theory 68n18-functional-programming-and-lambda-calculus 68p25-data-encryption 94a60-cryptography %P 39--50 %R 10.1145/1411204.1411213 %T The Power of Pi %U http://dx.doi.org/10.1145/1411204.1411213 %X 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. %@ 9781595939197

@inproceedings{Oury2008Power, abstract = {{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.}}, added-at = {2019-03-01T00:11:50.000+0100}, address = {New York}, author = {Oury, Nicolas and Swierstra, Wouter}, biburl = {https://www.bibsonomy.org/bibtex/2abff186666b906014a4b39a2b651e45f/gdmcbain}, booktitle = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08}, citeulike-article-id = {4463383}, citeulike-attachment-1 = {oury_08_power.pdf; /pdf/user/gdmcbain/article/4463383/1131659/oury_08_power.pdf; ca6d59bcbf0c6366953614f0ff9b21d45ea91865}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1411204.1411213}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1411204.1411213}, comment = {For discussion at 'Sydney Type Theory':https://www.meetup.com/Sydney-Type-Theory/events/ggsjlmyxfbqb/, 2018-03-12}, doi = {10.1145/1411204.1411213}, file = {oury_08_power.pdf}, interhash = {fb74645358c4bac102d7c58f67188000}, intrahash = {abff186666b906014a4b39a2b651e45f}, isbn = {9781595939197}, keywords = {03b15-higher-order-logic-type-theory 68n18-functional-programming-and-lambda-calculus 68p25-data-encryption 94a60-cryptography}, location = {Victoria, BC, Canada}, pages = {39--50}, posted-at = {2018-03-11 22:37:18}, priority = {5}, publisher = {ACM Press}, timestamp = {2019-03-01T00:11:50.000+0100}, title = {The Power of {P}i}, url = {http://dx.doi.org/10.1145/1411204.1411213}, year = 2008 }