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:
- To demonstrate the advantages of doing sophisticated network
systems programming in advanced languages that provide garbage
collection, higher-order procedures, exceptions, module systems,
and "safe" compilers.
- To provide a pedagogical explication of the HTTP protocol.
- To provide a very flexible and extensible server for custom
applications not handled by the more commonly-used servers.
- To experiment with mobile code. The server allows for arbitrary
Scheme code to be safely uploaded into and executed by the server.
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.