1 July - 31 December 1995
Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)
Friday 3 November, 2:15 pm
Sandip K. Biswas (Pennsylvania)
Program Slicing, for first-order imperative programs, is an extensively researched area, with applications in debugging and testing of programs. A first-order imperative program is a sequence of statements. The control-flow graph of such programs can be inferred from the parse tree. A dynamic slice of a program P, with input I, is a subsequence Q, of statements of P, such that when Q is executed, with input I, the value returned is the same as that of P run on I.
Higher-order languages, like ML, differ from first-order imperative programs in two significant ways. Fistly, we do not have syntactic categories: statements and expressions. The entire program is an expression and deleting arbitrary sub-expressions no longer leaves behind an executable program. Hence, we redefine the deletion of a subexpression by replacement with a *no-op* term, and provide operational semantics for this extended language. Secondly, the control-flow is substantially more complicated, particularly, in the presence of exceptions.
If a core-ML term M, with assignments and exceptions, evaluates to a value/exception packet then we provide a proof system to compute the subterms of M which can be deleted, such that the deleted term, under the extended operational semantics, still evaluates to the same answer. This computation of subterms, which can be deleted, can be done by instrumenting the ML code of the original term.