Events

Materials and manufacturing processes can be made to adapt to the way in which their end-products are used, by imbuing raw materials with sensing and computation elements. By making the algorithms that run on these computing elements aware of the physics of the objects in which they are embedded, computation-and-sensing augmented materials could change the way we think about the border between inanimate objects and computing systems. One way to exploit knowledge about the physical world in the programs running on (or in) these objects is to exploit the fact that these programs can often tolerate noise and other deviations from correctness in their input data. This talk will highlight research that builds on these observations.

In this talk, I will present my work on simple distributed protocols for fundamental coordination problems such as plurality and valid consensus, rumor spreading and distributed clustering in stochastic models of interaction. I will discuss applications in the research area of Biological Distributed Algorithms, which aims to understand through the algorithmic lens, the collective behavior of biological systems, such as social insects. This setting has recently motivated the study of some interesting new problems, such as the investigation of systems where communication is affected by noise in a way which cannot be handled by error correction codes. More recently, as a fellow of the Simons Institute for the Theory of Computing, I have been working at the interface between Theoretical Computer Science and Computational Neuroscience. I will provide a brief overview of some research topics in this direction.

Sound static analysis over-approximates the set of all possible executions in a given program in order to prove the absence of errors in the program. Due to this over-approximation, sound static analysis may generate spurious warnings about executions that are not wrong or even possible in the program. To become more practical, many static analyzers give up soundness by design. This means that they do not check certain properties or that they check them under certain unsound assumptions, such as the absence of arithmetic overflow. At the other end of the soundness spectrum, we have automatic test-case generation, which typically under-approximates the set of possible program executions. The goal of test-case generation is not to prove the absence of errors in the program but, rather, their existence. In this talk, I will present an overview of my research on combining these program analysis techniques to improve their overall automation, performance, and accuracy on real programs.

We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.

We present each notion as an extension of a simply-typed core lambda-calculus with an effect type system. Using Felleisen's notion of a macro translation, we show that these abstractions can macro-express each other, providing we disregard types. Alas, not all of the translations are type-preserving; moreover, no alternative type-preserving macro translations exist. We show that if we add suitable notions of polymorphism to the core calculus and its extensions then all of the translations can be adapted to preserve typing.

(based on joint work with Yannick Forster, Ohad Kammar, and Matija Pretnar)