2 options
Linear/Non-linear Types for Embedded Domain-specific Languages / Jennifer Paykin.
- Format:
- Book
- Thesis/Dissertation
- Author/Creator:
- Paykin, Jennifer, author.
- Language:
- English
- Subjects (All):
- Computer science.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Local Subjects:
- Computer science.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Genre:
- Academic theses.
- Physical Description:
- 1 online resource (208 pages)
- Contained In:
- Dissertation Abstracts International 80-02B(E).
- Place of Publication:
- [Philadelphia, Pennsylvania] : University of Pennsylvania ; Ann Arbor : ProQuest Dissertations & Theses, 2018.
- Language Note:
- English
- System Details:
- Mode of access: World Wide Web.
- text file
- Summary:
- Domain-specific languages are often embedded inside of general-purpose host languages so that the embedded language can take advantage of host-language data structures, libraries, and tools. However, when the domain-specific language uses linear types, existing techniques for embedded languages fall short. Linear type systems, which have applications in a wide variety of programming domains including mutable state, I/O, concurrency, and quantum computing, can manipulate embedded non-linear data via the linear type !sigma. However, prior work has not been able to produce linear embedded languages that have full and easy access to host-language data, libraries, and tools.
- This dissertation proposes a new perspective on linear, embedded, domain-specific languages derived from the linear/non-linear (LNL) interpretation of linear logic. The LNL model consists of two distinct fragments---one with linear types and another with non-linear types---and provides a simple categorical interface between the two. This dissertation identifies the linear fragment with the linear embedded language and the non-linear fragment with the general-purpose host language.
- The effectiveness of this framework is illustrated via a number of examples, implemented in a variety of host languages. In Haskell, linear domain-specific languages using mutable state and concurrency can take advantage of the monad that arises from the LNL model. In Coq, the QWIRE quantum circuit language uses linearity to enforce the no-cloning axiom of quantum mechanics. In homotopy type theory, quantum transformations can be encoded as higher inductive types to simplify the presentation of a quantum equational theory. These examples serve as case studies that prove linear/non-linear type theory is a natural and expressive interface in which to embed linear domain-specific languages.
- Notes:
- Source: Dissertation Abstracts International, Volume: 80-02(E), Section: B.
- Advisors: Steve Zdancewic; Committee members: Benjamin Pierce; Andre Scedrov; Peter Selinger; Stephanie Weirich.
- Department: Computer and Information Science.
- Ph.D. University of Pennsylvania 2018.
- Local Notes:
- School code: 0175
- ISBN:
- 9780438424111
- Access Restriction:
- Restricted for use by site license.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.