A HoTT Approach to Computational Effects

Authors

Phillip A. Wells, The College of WoosterFollow

Abstract

A computational effect is any mutation of real-world state that occurs as the result of a computation. We develop a model for describing computational effects within homotopy type theory, a branch of mathematics separate from other foundations such as set theory. Such a model allows us to describe programs as total functions over values while preserving information about the effects those programs induce.

Advisor

Fox, Nathan

Department

Computer Science

Recommended Citation

Wells, Phillip A., "A HoTT Approach to Computational Effects" (2019). Senior Independent Study Theses. Paper 8566.
https://openworks.wooster.edu/independentstudy/8566

Disciplines

Theory and Algorithms

Keywords

homotopy, type theory, computation, theory

Publication Date

2019

Degree Granted

Bachelor of Arts

Document Type

Senior Independent Study Thesis Exemplar