TACL Seminar Spring '06

From CSWiki
Revision as of 15:00, 15 August 2006 by Ddantas (talk | contribs)

Jump to: navigation, search

TACL Seminar


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
May 17 Mike Hind (IBM) Online Performance Auditing: Using Hot Optimizations Without Getting Burned
May 18 Matthew Bridges Automatic Instruction Scheduler Retargeting by Reverse-Engineering


Limin Jia

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 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.

ChucK homepage:


Audicle homepage: