|
Senior Thesis 2024
Computer Science Department
School of Computer Science, Carnegie Mellon University
Memory Reuse in Linear Functional Computation
Daniel Ng
Senior Thesis
May 2024
Thesis Document
The semi-axiomatic sequent calculus, or SAX, offers an alternative way to represent proofs in the sequent calculus. SAX also corresponds to a process calculus, where processes interact by writing and reading from memory cells. Improvements were then made to the memory layout of data structures to create the SNAX language, which acts similarly to SAX but uses fewer pointer dereferences. We have now added a system of memory reuse to the existing linear system provided by SNAX, further minimizing the time spent performing memory allocations. We have also updated both the typing rules and the dynamic rules for SNAX to accommodate reuse. Unlike the original SNAX, which is concurrent, SNAX with reuse runs under a sequential semantics. With memory reuse, progress and preservation still hold, meaning that well-typed programs in SNAX will never cause a memory error. Our changes allow SNAX to more closely match other functional languages that are capable of updating their single-threaded data structures in-place.
36 pages
Advisor
Frank Pfenning
|