TACL Seminar Spring '06
|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||Specifying C++ Concepts||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|
ILC: A Foundation for Automated Reasoning About Pointer Programs
ChucK and Audicle: Programming Language and Environment for Sound Synthesis
We hope to make this an interesting and amusing presentation for all.
A Refined Kripke Semantics for Hard-to-Model Types
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.
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.