Showing 1–3 of 3 results for author: Johnson-Freyd, P

A Nominal Approach to Probabilistic Separation Logic

Authors: John M. Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, Steven Holtzen

Abstract: Currently, there is a gap between the tools used by probability theorists and those used in formal reasoning about probabilistic programs. On the one hand, a probability theorist decomposes probabilistic state along the simple and natural product of probability spaces. On the other hand, recently developed probabilistic separation logics decompose state via relatively unfamiliar measure-theoretic… ▽ More Currently, there is a gap between the tools used by probability theorists and those used in formal reasoning about probabilistic programs. On the one hand, a probability theorist decomposes probabilistic state along the simple and natural product of probability spaces. On the other hand, recently developed probabilistic separation logics decompose state via relatively unfamiliar measure-theoretic constructions for computing unions of sigma-algebras and probability measures. We bridge the gap between these two perspectives by showing that these two methods of decomposition are equivalent up to a suitable equivalence of categories. Our main result is a probabilistic analog of the classic equivalence between the category of nominal sets and the Schanuel topos. Through this equivalence, we validate design decisions in prior work on probabilistic separation logic and create new connections to nominal-set-like models of probability. △ Less

Submitted 28 May, 2024; v1 submitted 10 May, 2024; originally announced May 2024.

Topos Semantics for a Higher-Order Temporal Logic of Actions

Authors: Philip Johnson-Freyd, Jon Aytac, Geoffrey Hulette

Abstract: TLA is a popular temporal logic for writing stuttering-invariant specifications of digital systems. However, TLA lacks higher-order features useful for specifying modern software written in higher-order programming languages. We use categorical techniques to recast a real-time semantics for TLA in terms of the actions of a group of time dilations, or "stutters," and an extension by a monoid inco… ▽ More TLA is a popular temporal logic for writing stuttering-invariant specifications of digital systems. However, TLA lacks higher-order features useful for specifying modern software written in higher-order programming languages. We use categorical techniques to recast a real-time semantics for TLA in terms of the actions of a group of time dilations, or "stutters," and an extension by a monoid incorporating delays, or "falters." Via the geometric morphism of the associated presheaf topoi induced by the inclusion of stutters into falters, we construct the first model of a higher-order TLA. △ Less

Submitted 14 September, 2020; originally announced September 2020.

Comments: In Proceedings ACT 2019, arXiv:2009.06334

Journal ref: EPTCS 323, 2020, pp. 161-171

First Class Call Stacks: Exploring Head Reduction

Authors: Philip Johnson-Freyd, Paul Downen, Zena M. Ariola

Abstract: Weak-head normalization is inconsistent with functional extensionality in the call-by-name $λ$-calculus. We explore this problem from a new angle via the conflict between extensionality and effects. Leveraging ideas from work on the $λ$-calculus with control, we derive and justify alternative operational semantics and a sequence of abstract machines for performing head reduction. Head reduction av… ▽ More Weak-head normalization is inconsistent with functional extensionality in the call-by-name $λ$-calculus. We explore this problem from a new angle via the conflict between extensionality and effects. Leveraging ideas from work on the $λ$-calculus with control, we derive and justify alternative operational semantics and a sequence of abstract machines for performing head reduction. Head reduction avoids the problems with weak-head reduction and extensionality, while our operational semantics and associated abstract machines show us how to retain weak-head reduction's ease of implementation. △ Less

Submitted 20 June, 2016; originally announced June 2016.

Comments: In Proceedings WoC 2015, arXiv:1606.05839

ACM Class: F.3.2; F.3.3

Journal ref: EPTCS 212, 2016, pp. 18-35