September 14 '95 Seminar Minutes

Attendance

About 20 people attended the seminar.

10:00am Karen Bernstein: Debugging Type Errors

Type inferencing is very effective for finding certain types of programming errors at compile-time. Because these errors can be quite complex, the diagnostic messages generated by the type inferencing algorithm can be hard to understand. We show that by extending the type inferencing algorithm for Standard ML to infer types for open terms, we can provide a "debugger" for type errors. This "debugger" allows the programmer to "set breakpoints" and extract types for pieces of programs. This talk will cover some of the issues involved in debugging type errors as well as our proposed extension to the Standard ML programming environment.

11:00am Sandip Biswas: Dynamic Slicing of Higher-Order Programs

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.

12:00 am John Reppy: Simple objects for SML

This talk will describe some ideas about adding "objects" to SML, which Jon Riecke and I are exploring. Our approach is simple, in the sense that it requires only a small conservative extension to the Damas-Milner type system.

1:45 pm Lal George: Admin

2:00 pm Mourad Debbabi: An Effect-Based CFA for Higher-Order Concurrent Programs

In this talk, we address the problem of control-flow analysis for concurrent and functional languages. More accurately, we present an effect-based type system that propagates not only the type of programs but also their effects and call graphs. The type system operates on an ML core-syntax extended with higher-order concurrency primitives. Call graphs are captured by an algebra that is close to usual process algebras and is endowed with a simulation relation. Furthermore, the static semantics uses subtyping in order to ensure a good flexibility of the type system. We present the typing rules as well as the reconstruction algorithm. The latter is based on a syntactic unification modulo the propagation and the resolution of type, effect and graph constraints.

3:00 pm Olin Shivers: Web Server

I will describe the structure of a Web server I have recently constructed in Scheme 48. This talk will be in part an introduction to some of the details of the Web infrastructure. The server was written with a few primary goals:

Beyond describing how the server fulfills these goals, I will also seek to motivate interested parties to investigate the application of advanced languages to network applications.

Documentation and full sources for the server are available.