Content deleted Content added
wikif. |
→Refinement types: cite |
||
Line 19:
== Refinement types ==
In [[type theory]], a '''refinement type'''<ref>{{cite conference|first1=T.|last1=Freeman|first2=F.|last2=Pfenning|url=ftp://ftp.cs.cmu.edu/usr/rwh/www/home/courses/refinements/papers/Freeman94/phd.pdf|doi=10.1145/113445.113468 |title=Refinement types for ML|booktitle=Proceedings of the ACM Conference on Programming Language Design and Implementation|pages=268–277|year=1991}}</ref><ref>{{cite conference|first=S.|last=Hayashi|title=Logic of refinement types|url=http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.6346&rep=rep1&type=pdf#page=167|doi=10.1007/3-540-58085-9_74|booktitle=Proceedings of the Workshop on Types for Proofs and Programs|pages=157–172|year=1993}}</ref><ref>{{cite conference|first=E.|last=Denney|url=http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.22.4988&rep=rep1&type=pdf|title=Refinement types for specification|booktitle=Proceedings of the IFIP International Conference on Programming Concepts and Methods|volume=125|pages=148–166|publisher=Chapman & Hall|year=1998}}</ref> is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express [[precondition]]s when used as [[function argument]]s or [[postcondition]]s when used as [[return type]]s: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as <math>f: \mathbb{N} \rarr \{n: \mathbb{N} | n > 5\}</math>. Refinement types are thus related to [[behavioral subtyping]].
== References ==
| |||