Publications

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 higherorder 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.

Modern programming languages have effects and mix multiple calling conventions, and their core calculi should too. We characterize calling conventions by their “substitution discipline” that says what variables stand for, and design calculi for mixing disciplines in a single program. Building on variations of the reducibility candidates method, including biorthogonality and symmetric candidates which are both specialized for one discipline, we develop a single uniform framework for strong normalization encompassing call-by-name, call-by-value, call-by-need, call-by-push-value, non-deterministic disciplines, and any others satisfying some simple criteria. We explicate commonalities of previous methods and show they are special cases of the uniform framework and they extend to multi-discipline programs.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.