Should your specification language be typed Export

@article{shouldbetyped:lamporrt:acm:1997, abstract = {Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has been widely overlooked, offers many advantages. Untyped set theory is simple and is more flexible than any simple typed formalism. Polymorphism, overloading, and subtyping can make a type system more powerful, but at the cost of increased somplexity, and such refinements can never attain the flexibility of having no types at all. Typed formalisms have advantages, too, stemming from the power of mechanical type checking. While types serve little purpose in hand proofs, they do help with mechanized proofs. In the absence of verificaiton, type checking can catch errors in specifications. It may be possible to have the best of both worlds by adding typing annotations to an untyped specification language. We consider only specification languages, not programming languages.}, address = {New York, NY, USA}, author = {Lamport, Leslie and Paulson, Lawrence C.}, citeulike-article-id = {6095490}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=319301.319317}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/319301.319317}, doi = {10.1145/319301.319317}, issn = {0164-0925}, journal = {ACM Trans. Program. Lang. Syst.}, keywords = {lamport, mechanical\_type, programming\_languages, specification\_languages, tlaplus}, number = {3}, pages = {502--526}, posted-at = {2009-11-10 17:42:28}, priority = {2}, publisher = {ACM}, title = {Should your specification language be typed}, url = {http://dx.doi.org/10.1145/319301.319317}, volume = {21}, year = {1999} }

TY - JOUR ID - shouldbetyped:lamporrt:acm:1997 L3 - citeulike-article-id:6095490 N2 - Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has been widely overlooked, offers many advantages. Untyped set theory is simple and is more flexible than any simple typed formalism. Polymorphism, overloading, and subtyping can make a type system more powerful, but at the cost of increased somplexity, and such refinements can never attain the flexibility of having no types at all. Typed formalisms have advantages, too, stemming from the power of mechanical type checking. While types serve little purpose in hand proofs, they do help with mechanized proofs. In the absence of verificaiton, type checking can catch errors in specifications. It may be possible to have the best of both worlds by adding typing annotations to an untyped specification language. We consider only specification languages, not programming languages. IS - 3 JF - ACM Trans. Program. Lang. Syst. SN - 0164-0925 AD - New York, NY, USA EP - 526 TI - Should your specification language be typed PB - ACM VL - 21 SP - 502 KW - lamport KW - mechanical_type KW - programming_languages KW - specification_languages KW - tlaplus AU - Lamport, Leslie AU - Paulson, Lawrence PY - 1999/// UR - http://dx.doi.org/10.1145/319301.319317 ER -