35 lines
3.5 KiB
BibTeX
35 lines
3.5 KiB
BibTeX
@book{tapl,
|
|
author = {Pierce, Benjamin C.},
|
|
title = {Types and Programming Languages},
|
|
year = {2002},
|
|
isbn = {0262162091},
|
|
publisher = {The MIT Press},
|
|
edition = {1st},
|
|
abstract = {A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to the kinds of values they compute. The study of type systems -- and of programming languages from a type-theoretic perspective -- has important applications in software engineering, language design, high-performance compilers, and security.This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Each chapter is accompanied by numerous exercises and solutions, as well as a running implementation, available via the Web. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material.The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators. Extended case studies develop a variety of approaches to modeling the features of object-oriented languages.}
|
|
}
|
|
|
|
@article{gator,
|
|
author = {Geisler, Dietrich and Yoon, Irene and Kabra, Aditi and He, Horace and Sanders, Yinnon and Sampson, Adrian},
|
|
title = {Geometry types for graphics programming},
|
|
year = {2020},
|
|
issue_date = {November 2020},
|
|
publisher = {Association for Computing Machinery},
|
|
address = {New York, NY, USA},
|
|
volume = {4},
|
|
number = {OOPSLA},
|
|
url = {https://doi.org/10.1145/3428241},
|
|
doi = {10.1145/3428241},
|
|
abstract = {In domains that deal with physical space and geometry, programmers need to track the coordinate systems that underpin a computation. We identify a class of geometry bugs that arise from confusing which coordinate system a vector belongs to. These bugs are not ruled out by current languages for vector-oriented computing, are difficult to check for at run time, and can generate subtly incorrect output that can be hard to test for. We introduce a type system and language that prevents geometry bugs by reflecting the coordinate system for each geometric object. A value's geometry type encodes its reference frame, the kind of geometric object (such as a point or a direction), and the coordinate representation (such as Cartesian or spherical coordinates). We show how these types can rule out geometrically incorrect operations, and we show how to use them to automatically generate correct-by-construction code to transform vectors between coordinate systems. We implement a language for graphics programming, Gator, that checks geometry types and compiles to OpenGL's shading language, GLSL. Using case studies, we demonstrate that Gator can raise the level of abstraction for shader programming and prevent common errors without inducing significant annotation overhead or performance cost.},
|
|
journal = {Proc. ACM Program. Lang.},
|
|
month = nov,
|
|
articleno = {173},
|
|
numpages = {25},
|
|
keywords = {computer graphics, geometry, language design, type systems}
|
|
}
|
|
|
|
@inproceedings{Siek2006GradualTF,
|
|
title={Gradual Typing for Functional Languages},
|
|
author={Jeremy G. Siek and Walid Taha},
|
|
year={2006},
|
|
url={https://api.semanticscholar.org/CorpusID:1398902}
|
|
} |