-
Amortized Analysis as a Cost-Aware Abstraction Function
Data structures contain two important aspects that computer scientists seek to verify: behavior and cost. The behavior of data structures has long been studied using abstraction functions, which translate concrete data structure representations into a semantic representation. On the other hand, the cost associated with data structures has been analyzed using the method of amortization, a technique in which cost is studied in aggregate: rather than considering the maximum cost of a single operation, one bounds the total cost encountered throughout a sequence of operations. In this post, I will demonstrate how to unify these two techniques, packaging the data associated with an amortized analysis as an abstraction function that incorporates cost. This reframing is more amenable to formal verification, consolidates prior variations of amortized analysis, and generalizes amortization to novel settings.
-
Poly-morphic effect handlers
In computer science, programmers often perform effects to interact with the surrounding environment. For example, a program may print strings or interact with mutable state. Then, effects may be handled, implemented in terms of other effects. In this post, we reconstruct a categorical semantics for programs with effects, and we isolate a class of composable effect handlers that may be concisely described in the language of polynomial functors, the free monad monad, and the Grothendieck construction.
-
Recursive Types via Domain Theory
Functional programming languages often include recursive types, allowing programmers to define types satisfying a given isomorphism. Such types cannot all be interpreted as sets, but they can be understood using domain theory. We consolidate and present foundational techniques in domain theory to understand eager programming languages with recursive types from a categorical perspective. We define a category of domains with finite coproducts, a symmetric monoidal closed structure for eager products and functions, and least solutions of recursive domain equations, whose objects are retracts of a universal space and whose morphisms are continuous with respect to a topology of approximations.
-
Serializing to JSON in SML/NJ
The SML/NJ standard library includes utilities for working with JSON. In this post, we outline the essentials and demonstrate simple usage examples.
