2026-09-18T18:37:12Zhttps://ecommons.cornell.edu/server/oai/requestoai:ecommons.cornell.edu:1813/1164552026-05-15T19:51:22Zcom_1813_35col_1813_47
Geisler, Dietrich
Sampson, Adrian
Marschner, Stephen
Foster, John
Martinez, Jose
2025-01-14T19:59:22Z
2025-01-14T19:59:22Z
2024-08
ProQuest Submission ID: 14574
ProQuest Publication ID: 31488511
https://hdl.handle.net/1813/116455
https://doi.org/10.7298/reh0-tm98
16611659
169 pages
There has been growing demand for graphical image rendering in the past several decades. This demand has arisen primarily in video games, but also from fields as broad as film, art, architecture, and scientific simulation. A major challenge with expanding use of rendering, however, is that graphics programming is difficult, requiring significant field expertise when abstractions break down. In this dissertation, we will examine how we may be able to design programming languages to ameliorate some of these challenges. Our goal will be to examine two specific difficulties in graphics programming reasoning: geometric correctness and performance in heterogeneous device communication. In the first chunk of this dissertation, we will examine Gator, a language which provides type-level reasoning for a class of bugs we describe as "geometry bugs", as well as a lightweight mechanism to reason about operations on geometry. In the second chunk of this dissertation, we will discuss Caiman, a language which typechecks heterogeneous implementations against a fixed specification. We will also examine how Caiman's type-level restrictions allow for separating performance and correctness, as well as providing a mechanism for restricted synthesis of heterogeneous programs.
en
Attribution-ShareAlike 4.0 International
https://creativecommons.org/licenses/by-sa/4.0/
Compilers
Graphics
Programming Languages
Language Designs for Geometry and Heterogeneous Reasoning in Graphics Programming
dissertation or thesis
https://newcatalog.library.cornell.edu/catalog/16611659
application/pdf
Computer Science
Cornell University
Doctor of Philosophy
Ph. D., Computer Science
https://hdl.handle.net/1813/59810.2
Publication
Cornell Theses and Dissertations
Geisler, Dietrich
5893a6ea-7af3-41d7-abc6-04bcd26ab5df
open.access
open.access
<Publication xmlns="https://www.openaire.eu/cerif-profile/1.1/" id="063759fe-42c6-4352-9240-52657a65be90">
<Type xmlns="https://www.openaire.eu/cerif-profile/vocab/COAR_Publication_Types">http://purl.org/coar/resource_type/c_1843</Type>
<Language>en</Language>
<Title>Language Designs for Geometry and Heterogeneous Reasoning in Graphics Programming</Title>
<PublishedIn>
<Publication>
</Publication>
</PublishedIn>
<PublicationDate>2024-08</PublicationDate>
<DOI>https://doi.org/10.7298/reh0-tm98</DOI>
<Authors>
<Author>
<DisplayName>Geisler, Dietrich</DisplayName>
<Affiliation>
<OrgUnit>
</OrgUnit>
</Affiliation>
</Author>
</Authors>
<Editors>
</Editors>
<Publishers>
<Publisher>
<OrgUnit />
</Publisher>
</Publishers>
<License>https://creativecommons.org/licenses/by-sa/4.0/</License>
<Keyword>Compilers</Keyword>
<Keyword>Graphics</Keyword>
<Keyword>Programming Languages</Keyword>
<Abstract>There has been growing demand for graphical image rendering in the past several decades. This demand has arisen primarily in video games, but also from fields as broad as film, art, architecture, and scientific simulation. A major challenge with expanding use of rendering, however, is that graphics programming is difficult, requiring significant field expertise when abstractions break down. In this dissertation, we will examine how we may be able to design programming languages to ameliorate some of these challenges. Our goal will be to examine two specific difficulties in graphics programming reasoning: geometric correctness and performance in heterogeneous device communication. In the first chunk of this dissertation, we will examine Gator, a language which provides type-level reasoning for a class of bugs we describe as "geometry bugs", as well as a lightweight mechanism to reason about operations on geometry. In the second chunk of this dissertation, we will discuss Caiman, a language which typechecks heterogeneous implementations against a fixed specification. We will also examine how Caiman's type-level restrictions allow for separating performance and correctness, as well as providing a mechanism for restricted synthesis of heterogeneous programs.</Abstract>
<Access xmlns="http://purl.org/coar/access_right"
>
</Access>
</Publication>