ABSTRACT. We need to reason about low-level programs because they are what actually runs on our machines. As low-level languages tend to be messy and complex, so does proving things about them. But a slightly subtler and more interesting problem is that the things we want to prove about such programs are often phrased in terms of high-level notions, such as being a valid implementation of a particular function, or behaving like something with a particular high-level type. It can be far from obvious how to even translate such specifications into terms that make sense at the low level, let alone verify that programs meet them. I’ll discuss the problem, and ways it can be addressed, drawing on examples from compositional correctness and type soundness of compilers, and the design of logics for low-level programs.

ABSTRACT. We describe a new framework for self-modifying programs. Our goal is to show how to extract program abstraction focusing on self-modifications. On the first hand, we use a abstract machine which makes explicit some typical behavior, such as turning data into executable code and vice versa. Moreover memory is also separated between data (what we can read and write) and code (what we can execute). On the other hand, we add another level of granularity in memory location, in order to build a more static program abstraction.

ABSTRACT. Effect handling is a novel paradigm in programming that complements the established algebraic approach to programming with effects. Intuitively, algebraic effects are those which distribute over sequential composition and hence can affect the control flow only in a quite conservative fashion. Effect handling, by contrast, allows for expressing more powerful constructions, the most basic example being exception handling. More generally, effect handling can be viewed as a lightweight, well-behaved alternative to control operations like call/cc. We develop novel semantic foundations for effect handling in the presence of iteration, based on cofree extensions of monads. In the larger perspective we view our current work as a prerequisite for designing a generic relatively complete Hoare calculus from programs with algebraic effects, iteration and handling.

ABSTRACT. Tensorial logic is a primitive logic of tensor and negation which refines linear logic by relaxing the hypothesis that negation is involutive. One reason for introducing the logic is that its proof-nets coincide with innocent strategies between dialogue games. In this talk, we explain how to extend tensorial logic with various notions of algebraic effects. By way of illustration, we establish that the resulting notion of tensorial proof net coincides in the particular case of local stores with the notion of visible strategy formulated by Abramsky and McCusker in their study of Idealized Algol.

ABSTRACT. We present a prototype implementation of the memoryful GoI framework of [Hoshino, Muroya and Hasuo, CSL-LICS 2014] that translates lambda terms with algebraic effects to transducers. Those transducers can be thought of as “proof nets with memories” and are constructed in a compositional manner by means of coalgebraic component calculi. The transducers thus obtained can be simulated in our tool, too, helping us to scrutinize the step-by-step interac- tions that take place in higher-order effectful computation.

ABSTRACT. Formal verification of programs and systems lacks a concept of objective and absolute correctness. One may only claim correctness with respect to a model. How detailed can we make this model? At which point does our desire for completeness infringe upon project tractability? For operating system verification in particular, overly naïve models result in poor performance and ineffective use of hardware features. On the other hand, overly complex models result in human resource exhaustion and a graveyard of ambitious projects that burnt out in the race for realism.

In this talk, I will discuss these tradeoffs based upon my long experience with the L4.verified project, a successful 20 person-year effort to verify the functional correctness of the seL4 microkernel. I will also discuss my own efforts in searching for an elegant semantics for reasoning about virtual memory based on separation logic.

ABSTRACT. Most compiler correctness efforts, whether based on validation or once-and-for-all verification, are tightly tied to the particular language(s) under consideration. Proof techniques may be replicated for other targets, and parts of the compiler chain may be shared for new input or output languages, but the extent to which common elements can be generalized across multiple targets has not been fully explored. In this paper, we lay out a general approach to specifying and verifying optimizations and transformations on low-level intermediate languages. By generalizing across elements such as concurrent memory models and single-thread operational semantics, we can build a library of facts that can be reused in verifying optimizations for dramatically different target languages, such as stack-machine and register-machine languages.

ABSTRACT. In game semantics and related approaches to programming language semantics, programs are modelled by interaction dialogues. Such models have recently been used by a number of authors for the design of compilation methods, in particular for applications where resource control is important. The work in this area has focused on call-by-name languages. In this talk I will consider the compilation of call-by-value into a first-order target language by means of an interpretation in an interactive model. The main result is that Plotkin’s standard call-by-value CPS-translation and its soundness proof can be refined to target this intermediate language. This refined CPS-translation amounts to a direct compilation of the source language into a first-order language.