Difference between revisions of "TACL Seminar Spring '06"

From CSWiki
Jump to: navigation, search
Line 41: Line 41:
This includes joint work with Andrew Appel, Paul-Andre Mellies, and Jerome Vouillon.
This includes joint work with Andrew Appel, Paul-Andre Mellies, and Jerome Vouillon.
[[TACL Seminar]]
[[TACL Seminar]]

Revision as of 15:04, 15 August 2006

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

Chris Richards

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.

TACL Seminar