Source author record

Gershom Bazerman

Gershom Bazerman appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science math.LO Programming Languages

Catalog footprint

What is connected

2works

3topics

1close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures

Functors with an instance of the Traversable type class can be thought of as data structures which permit a traversal of their elements. This has been made precise by the correspondence between traversable functors and finitary containers (also known as polynomial functors) -- established in the context of total, necessarily terminating, functions. However, the Haskell language is non-strict and permits functions that do not terminate. It has long been observed that traversals can at times in fact operate over infinite lists, for example in distributing the Reader applicative. The result of such a traversal remains an infinite structure, however it nonetheless is productive -- i.e. successive amounts of finite computation yield either termination or successive results. To investigate this phenomenon, we draw on tools from guarded recursion, making use of equational reasoning directly in Haskell.

preprint2020arXiv

The Topological and Logical Structure of Concurrency and Dependency via Distributive Lattices

This paper is motivated by the desire to study package management using the toolkit of the semantics of functional languages. As it transpires, this is deeply related to the semantics of concurrent computation. The models we produce are not solely of theoretical interest, but amenable to analysis and computation. This work makes a number of related contributions. First, it relates the specification of branching dependency structures, which exist in fields from knowledge-representation to package management, to the specification of semantics of concurrent computation. Second, it relates dependency structures to lattices in a precise way, establishing a full correspondence with a particular subclass of lattices. It then makes use of this as a key ingredient, coupled with the underappreciated Bruns-Lakser completion, in relating dependency structures to locales -- objects equipped with both topological and logical properties. It then provides an example of how this interplay of properties can be of use -- using topological properties of the dependency structure to equip internal logics of associated locales with a modality representing contraction relations (i.e. "versioning"). This approach lets us see linking (or rather, the choice of what to link against, i.e. "solving") as an effect. Finally, it discusses how such constructions may relate to important questions in complexity theory, including solutions of satisfiability problems. Along the way, we will see how this approach relates to familiar objects such as package version policies, Merkle-trees, the nix operating system, and distributed version control tooling like git.