ABSTRACT. The notion of asynchronous game was introduced by the author fifteen years ago in order to investigate the causal structure of innocent strategies in game semantics. Shifting from traditional sequential games to asynchronous games was the critical step behind the discovery of a number of important structural properties of games and logic. This includes a truly concurrent formulation of innocence based on local confluence diagrams, and a positionality theorem for innocent strategies. Asynchronous games also played a central role in the emergence of tensorial logic as the logic of dialogue games, in the same way as linear logic is the logic of proof nets. Since its origins, one guideline of the theory has been the observation that asynchronous games and asynchronous strategies are causal structures of the very same nature: in other words, asynchronous strategies are asynchronous games themselves, appropriately mapped into other asynchronous games. In this paper, we develop this simple idea one step further, and explain how to recover and to compare a number of game semantics with different flavors (alternating and non alternating) from the same categorical combinatorics, performed in the category of small categories.

ABSTRACT. The seminal work of Moggi [6] identified the abstract structure of computational effects as that given by the categorical concept of a monad. Plotkin and Power [7] considered monads induced by algebraic theories from this computational viewpoint and developed a theory of algebraic effects. The second-order algebraic theories of Fiore et al [2, 3] are a conservative extension of the algebraic theories of universal algebra that provide algebraic foundations for simple type theories with variable binding. The theme of this talk is to consider and study them from the perspective of computational effects. Fiore and Staton [5] gave a computational interpretation of the second-order algebraic theory of the substitution algebras of Fiore et al [4] as jump effects. I will introduce more general second-order algebraic theories of inception algebras and equip them with computational interpretations as control effects. These will be justified by a CPS semantics and then related to de Groote's computational interpretation of negation elimination and the excluded middle [1] and to Thielecke's CPS calculus [8]. Computational interpretations of second-order algebraic theories of the lambda calculus will also be considered. In particular, left lambda algebras will be shown to correspond to a coroutine mechanism.

References

[1] P. de Groote. A Simple Calculus of Exception Handling. In Proc. TLCA'95, LNCS 902, 1995.

[2] M. Fiore and C.-K. Hur. Second-order equational logic. In Proc. CSL 2010, LNCS 6247, 2010.

[3] M. Fiore and O. Mahmoud. Second-order algebraic theories. In Proc. MFCS 2010, LNCS 6281, 2010.

[4] M. Fiore, G. Plotkin and D. Turi. Abstract syntax and variable binding. In Proc. LICS'99, 1999.

[5] M. Fiore and S. Staton. Substitution, Jumps, and Algebraic Effects. In Proc. CSL-LICS'14, 2014.

[6] E. Moggi. Notions of computation and monads. Information and Computation 93, 1991.

[7] G. Plotkin and A.J. Power. Notions of computation determine monads. In Proc. FOSSACS'02, LNCS 2303, 2002.

[8] H. Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997.

ABSTRACT. The proposed talk describes ongoing work on modeling subregister aliasing in the CompCert formally verified~C compiler. We discuss some possible ways of modeling paired subregisters and their trade-offs. Exploring the design space uncovered long-standing fundamental type errors in CompCert's semantic models; implementing the eventual solution uncovered some more. We are close to finishing a new semantic model in which registers and stack slots are no longer treated as containing symbolic values but tuples of bytes.

ABSTRACT. .

ABSTRACT. This preliminary report studies a graphical version of Plotkin's call-by-value equational theory, in particular its soundness with respect to operational semantics. Although an equational theory is useful in safe program transformation like compiler optimisation, proving its soundness is not trivial, because it involves analysis of interaction between evaluation flow and a particular sub-program of interest. We observe that soundness can be proved in a direct and generic way in the graphical setting, using small-step semantics given by a graph-rewriting abstract machine previously build for evaluation-cost analysis. This would open up opportunities to think of a cost-sensitive equational theory for compiler optimisation, and to prove contextual equivalence directly in the presence of language extensions.

ABSTRACT. We describe a semantic differencing tool used to compare the bytecodes generated by two different compilers for Hack/PHP at Facebook. The tool is a prover for a simple relational Hoare logic for low-level code and is used in testing, allowing the developers to focus on semantically significant differences between the outputs of the two compilers.

ABSTRACT. We present a new methodology to model relaxed memory, interpreting a program on a given architecture by an event structure, expressing the causality between instructions, according to the optimisations performed by the hardware. The methodology uses standard tools of event structure theory, in particular product of event structures and the correspondence between event-based and execution-based representations.

In the talk, we will demonstrate the methodology on a simple weak memory specification: TSO (corresponding to Intel x86 processors). We will then present two applications of this model: one theoretical, showing a strong DRF guarantee, and another, more practical, showing how the model allows tinkering to generate smaller program representation than the state of the art.

ABSTRACT. We model exceptions in a linear, effectful setting by relaxing the notion of monadic strength to contexts that are discardable, in the spirit of C++ destructors. We find a ressource modality in linear call-by-push-value, that recalls unique_ptr/Box and move semantics in C++11 and Rust. This resource modality gives rise to an ordered logic in which symmetry (move) and weakening (drop) are available as effectful operations. We explore consequences in language design for resource management in functional programming languages. (2-page abstract)

ABSTRACT. In this work, we formalized in Agda graded monads, type and grade inference for computational lambda calculus with a graded monad, instantiate this for three kinds of effect and prove correct a number of program equivalences that depend on grading - to try out the use of graded monads for reasoning about programs in practice.

(We submitted the same abstract to TYPES 2018, which is a similar informal workshop with no publication.)

ABSTRACT. We give a denotational semantics of a first-order language with references, in which a computation denotes a dependent partial function. Heaps are represented as finitely partitioned trees.