N. Oury, and W. Swierstra. Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08, page 39--50. New York, ACM Press, (2008)
DOI: 10.1145/1411204.1411213
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.
%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
}