[PRL] Date change: Torture chamber next Wednesday (3/18)

[Stevie Strickland]

On Mar 14, 2009, at 9:58 PM, Stevie Strickland wrote:
> On Mar 10, 2009, at 6:12 PM, Stevie Strickland wrote:
>> I've reserved 366 for 3/16 from 12:00-1:30 so that I can run through
>> my upcoming ESOP talk.
>
> Actually, I'm going to use this time for a smaller initial run-through
> before I give a formal torture chamber on Wednesday afternoon.  So
> while anyone's free to come on Monday if they wish, the "real" one is
> Wednesday afternoon.
>
> (Currently I have 366 from 2:30-4:00, but I believe that Aaron may be
> giving his as well, and if so, then we'll likely start at 1:30  
> instead.)

Instead of moving it forward, we're moving it back due to other  
conflicts.  So here's the final information:

Wednesday, 3/18, 3:30-6:00

First will be Aaron's talk:

We introduce the All-Termination(T) problem: given a termination
solver T and a collection of functions F, find every subset of the
formal parameters to F whose consideration is sufficient to show,
using T, that F terminates. An important and motivating application is
enhancing theorem proving systems by constructing the set of strongest
induction schemes for F, modulo T. These schemes can be derived from
the set of termination cores, the minimal sets returned by
All-Termination(T), without any reference to an explicit measure
function. We study the All-Termination(T) problem as applied to the
size-change termination analysis (SCT), a PSpace-complete problem that
underlies many termination solvers. Surprisingly, we show that
All-Termination(SCT) is also PSpace-complete, even though it
substantially generalizes SCT. We develop a practical algorithm for
All-Termination(SCT), and show experimentally that on the ACL2
regression suite (whose size is over 100MB) our algorithm generates
stronger induction schemes on 90% of multiargument functions.

Then my talk:

Just as some functions have uniform behavior over distinct types,
other functions have uniform behavior over distinct arities.  These
variable-arity functions are widely used in scripting languages such
as Scheme and Python. Statically typed languages also accommodate
modest forms of variable-arity functions, but even ML and Haskell,
languages with highly expressive type systems, cannot type check the
wide variety of variable-arity functions found in untyped functional
languages. Consequently, their standard libraries contain numerous  
copies of
the same function definition with slightly different names.

As part of the Typed Scheme project---an on-going effort to create an
explicitly typed sister language for PLT Scheme---we have designed and
implemented an expressive type system for variable-arity
functions.  Our practical validation in the context of our extensive
code base confirms the usefulness of the enriched type system.

Thanks,
Stevie