ompositionality of Round Abstraction Abstract Dan R. Ghica and Mohamed N. Menaa University of Birmingham, U.K. We revisit a technique called round abstraction as a solution to the problem of building low-latency synchronous systesm from asynchronous specifications. We use a trace-semantic setting akin to Abramsky's Interaction Categories, which is also a generalisation of pointer-free game semantic models. We define partial and total correctness for round ion relative to composition and note that in its most general case, round abstraction can lead to incorrect behaviour. We then identify sufficient properties to guarantee partially correct composition. Finally, we a framework for round abstraction that is totally correct when applied to asynchronous behaviours. We apply this procedure to the Geometry of Synthesis, a technique for compiling higher-order imperative programming languages into digital circuits using game semantics.
Dan R. Ghica, Mohamed N. Menaa