# TACL Seminar Spring '06

## Schedule

Date | Speaker | Title | Links |
---|---|---|---|

Mar 1 | Limin Jia and Frances Spalding | Automated Reasoning about Pointer Programs using Linear Logic | |

Mar 8 | Limin Jia | ILC: A Foundation for Automated Reasoning About Pointer Programs | Abstract |

Apr 5 | Ge Wang | ChucK and Audicle: Programming Language and Environment for Sound Synthesis | Abstract |

Apr 10 | Chris Richards | A Refined Kripke Semantics for Hard-to-Model Types | Abstract |

Apr 11 | Bjarne Stroustrup - AT&T | Specifying C++ Concepts | Abstract |

May 17 | Mike Hind - IBM | Online Performance Auditing: Using Hot Optimizations Without Getting Burned | Abstract |

May 18 | Matthew Bridges | Automatic Instruction Scheduler Retargeting by Reverse-Engineering |

## Abstracts

### Limin Jia

**ILC: A Foundation for Automated Reasoning About Pointer Programs**

This paper shows how to use Girard's intuitionistic linear logic extended with a classical sublogic to reason about pointer programs. More specifically, first, the paper defines the proof theory for ILC (Intuitionistic Linear logic with Constraints) and shows it is well-defined via a proof of cut elimination. Second, inspired by prior work of O'Hearn, Reynolds, and Yang, the paper explains how to interpret linear logical formulas as descriptions of a program store. Third, this paper defines a simple imperative programming language with mutable references and arrays and gives verification condition generation rules that produce assertions in ILC. Finally, we identify a fragment of ILC, ILC$^{-}$, that is both decidable and closed under generation of verification conditions. Since verification condition generation is syntax-directed, we obtain a decidable procedure for checking properties of pointer programs.

### Ge Wang

**ChucK and Audicle: Programming Language and Environment for Sound Synthesis**

ChucK is a domain-specific programming language for real-time sound synthesis; the Audicle is a graphical development environment for programming ChucK "on-the-fly", and for monitoring the ChucK virtual machine in real-time. Together, they form a theoretical and a practical framework for writing and experimenting with complex audio/multimedia programs that (1) have powerful control over time and concurrency, (2) can be created on-the-fly, and (3) can map many input media (MIDI, joystick, keyboard, network, etc.) to sound synthesis parameters. In this seminar we present the language and environment, and show how ChucK has evolved since the last ChucK TACL seminar (2003).

We hope to make this an interesting and amusing presentation for all.

### Chris Richards

**A Refined Kripke Semantics for Hard-to-Model Types**

In the semantic approach to proving a type system sound (relative to an operational semantics), we give mathematical interpretations to type constructors and typing judgments -- the latter in such a way as to imply safety -- and prove each typing rule as a lemma. Certain desirable features, such as recursive types, mutable references, and impredicative polymorphism, have been challenging to model, especially in combination. Drawing particularly on the indexed model of Ahmed, Appel, and Virga, I show a uniform way to handle these "problem types" using techniques from the semantics of modal logic, allowing well-typedness to be relative to worlds, or states of computation. I look especially to the logic of provability, which interprets the modal operator \Box as "it is provable that", and whose characteristic axiom reflects, in the model, an induction principle on worlds.

The resulting model is better modularized than its ancestor models, avoids some previous technical restrictions on quantified types, and applies equally well to lambda-calculus and von Neumann machine models of computation. We conjecture that our technique is suitable for any such model with a small-step operational semantics.

This includes joint work with Andrew Appel, Paul-Andre Mellies, and Jerome Vouillon.

### Bjarne Stroustrup

**Specifying C++ Concepts**

C++ templates are key to the design of current successful mainstream libraries and systems. They are the basis of programming techniques in diverse areas ranging from conventional general-purpose programming to software for safety-critical embedded systems. Current work on improving templates focuses on the notion of *concepts* (a type system for templates), which promises significantly improved error diagnostics and increased expressive power such as concept-based overloading and function template partial specialization. This paper presents C++ templates with an emphasis on problems related to separate compilation.

We consider the problem of how to express concepts in a precise way that is simple enough to be usable by ordinary programmers. In doing so, we expose a few weakness of the current specification of the C++ standard library and suggest a far more precise and complete specification. We also present a systematic way of translating our proposed concept definitions, based on use-patterns rather than function signatures, into constraint sets that can serve as convenient basis for concept checking in a compiler.