| dc.contributor |
Sabry, Amr |
|
| dc.creator |
Chen, Chao-Hong |
|
| dc.date |
2021-08-23T03:09:12Z |
|
| dc.date |
2021-08-23T03:09:12Z |
|
| dc.date |
2021-08 |
|
| dc.date.accessioned |
2023-02-24T18:26:43Z |
|
| dc.date.available |
2023-02-24T18:26:43Z |
|
| dc.identifier |
http://hdl.handle.net/2022/26738 |
|
| dc.identifier.uri |
http://localhost:8080/xmlui/handle/CUHPOERS/260299 |
|
| dc.description |
Thesis (Ph.D.) - Indiana University, School of Informatics, Computing, and Engineering, 2021 |
|
| dc.description |
From the informational perspective, programs that are usually considered as pure have effects, for example, the simply typed lambda calculus is considered as a pure language. However, β–reduction does not preserve information and embodies information effects. To capture the idea about pure programs in the informational sense, a new model of computation — reversible computation was proposed. This work focuses on type-theoretic approaches for reversible effect handling. The main idea of this work is inspired by compact closed categories. Compact closed categories are categories equipped with a dual object for every object. They are well-established as models of linear logic, concurrency, and quantum computing. This work gives computational interpretations of compact closed categories for conventional product and sum types, where a negative type represents a computational effect that “reverses execution flow” and a fractional type represents a computational effect that “allocates/deallocates space”. |
|
| dc.language |
en |
|
| dc.publisher |
[Bloomington, Ind.] : Indiana University |
|
| dc.rights |
This work is under a CC-BY license. You are free to copy and redistribute the material in any format, as well as remix, transform, and build upon the material as long as you give appropriate credit to the original creator, provide a link to the license, and indicate any changes made. |
|
| dc.rights |
https://creativecommons.org/licenses/by/4.0/ |
|
| dc.subject |
Abstract Machine |
|
| dc.subject |
Duality of Computation |
|
| dc.subject |
Reversible Programming |
|
| dc.subject |
Termination Proofs |
|
| dc.subject |
Type Isomorphisms |
|
| dc.title |
ALGEBRAIC INFORMATION EFFECTS |
|
| dc.type |
Doctoral Dissertation |
|