Speaking Skills

Domain-specific languages can improve ease-of-use, expressiveness and verifiability, but defining and using different DSLs within a single application remains difficult.

We introduce an approach for embedding DSLs in a common host language where the type of a piece of domain-specific code can specify which grammar governs it. Because this grammar is type-specific, but the block is delimited by the host language, we can guarantee that link-time conflicts cannot arise. These grammars can recursively include top-level expressions using special entry tokens that guarantee that the composition of the type-specific language and the host language is also sound. We argue that this approach occupies a previously-unexplored sweet spot providing high expressiveness and ease-of-use while guaranteeing safety. We introduce the design, provide examples, sketch the safety theorems and describe an ongoing implementation of this strategy in the Wyvern programming language.

Joint work with Jonathan Aldrich, Darya Kurilova, Benjamin Chung, Ligia Nistor and Alex Potanin.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

Bag of Words is a popular and successful framework for the task of activity classification in videos. In BoW we extract features, cluster them to learn a codebook of words, and then quantize each video by pooling the features. We address limitations of two fundamental aspects of this framework. First, we add structure to the clustering step to enable generalization across different execution styles. Second, we provide a method for pooling features in a structured way. In prior work, this pooling is done over pre-determined rigid cuboids. It is natural to consider pooling features over a video segmentation, but this produces a video representation of variable size. We propose a fixed size representation, Motion Words, where we pool features over supervoxels. To segment the video into supervoxels we propose a superpixel-based method, Globally Consistent Supervoxels, designed to preserve motion boundaries over the entire video. Evaluation on classification and retrieval tasks on two datasets shows that Motion Words achieves state-of-the-art performance. In addition to providing a more flexible support for capturing actions, the proposed method enables interpretation of the results, i.e. it provides understanding of why two videos are similar.

Joint work with Fernando De la Torre and Martial Hebert.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

In the last decade Separation logic has been very successful for reasoning about imperative programs making serious use of the heap. Previous extensions of Separation Logic to concurrent programming languages have made serious use of auxiliary variables, thus making it difficult to reuse specifications and proofs.

In this talk I will present a new extension of Separation logic for concurrent programs. The logic separates specifications of protocol safety from specifications of heap safety. Keeping these properties distinct leads to specifications and proofs that can easily be reused in many different concurrent contexts.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

Subscribe to Speaking Skills