%0 Report %1 citeulike:14361778 %A Vytiniotis, Dimitrios %A Weirich, Stephanie %B 8th Symp. on Trends in Functional Programming %D 2007 %K 68q60-specification-and-verification 68n15-programming-languages 03b15-higher-order-logic-type-theory %N 1.81 %P 4449+ %T Dependent Types: Easy as PIE %U http://www.seas.upenn.edu/\~sweirich/papers/tfp07.pdf %V 10 %X Dependent type systems allow for a rich set of program properties to be expressed and mechanically verified via type checking. However, despite their significant expres- sive power, dependent types have not yet advanced into mainstream programming languages. We believe the reason behind this omission is the large design space for dependently typed functional programming languages, and the consequent lack of ex- perience in dependently-typed programming and language implementations. In this newly-started project, we lay out the design considerations for a general-purpose, ef- fectful, functional, dependently-typed language, called PIE. The goal of this project is to promote dependently-typed programming to a mainstream practice.

@techreport{citeulike:14361778, abstract = {{Dependent type systems allow for a rich set of program properties to be expressed and mechanically verified via type checking. However, despite their significant expres- sive power, dependent types have not yet advanced into mainstream programming languages. We believe the reason behind this omission is the large design space for dependently typed functional programming languages, and the consequent lack of ex- perience in dependently-typed programming and language implementations. In this newly-started project, we lay out the design considerations for a general-purpose, ef- fectful, functional, dependently-typed language, called PIE. The goal of this project is to promote dependently-typed programming to a mainstream practice.}}, added-at = {2017-06-29T07:13:07.000+0200}, author = {Vytiniotis, Dimitrios and Weirich, Stephanie}, biburl = {https://www.bibsonomy.org/bibtex/276695ee699baf11036442be507b709a5/gdmcbain}, booktitle = {8th Symp. on Trends in Functional Programming}, citeulike-article-id = {14361778}, citeulike-attachment-1 = {vytiniotis_07_dependent.pdf; /pdf/user/gdmcbain/article/14361778/1110185/vytiniotis_07_dependent.pdf; c8f6aca251ad77abad9bb6b1f31bc480faeb1d26}, citeulike-linkout-0 = {http://www.seas.upenn.edu/\~{}sweirich/papers/tfp07.pdf}, file = {vytiniotis_07_dependent.pdf}, interhash = {71d75f51ef04a1328f79f2e757d2154b}, intrahash = {76695ee699baf11036442be507b709a5}, keywords = {68q60-specification-and-verification 68n15-programming-languages 03b15-higher-order-logic-type-theory}, month = apr, number = {1.81}, pages = {4449+}, posted-at = {2017-05-23 05:15:25}, priority = {2}, timestamp = {2019-04-01T03:34:56.000+0200}, title = {Dependent Types: Easy as {PIE}}, url = {http://www.seas.upenn.edu/\~{}sweirich/papers/tfp07.pdf}, volume = 10, year = 2007 }