N E P L S

These abstracts are for talks at this event. NEPLS is a venue for ongoing research, so the abstract and supplemental material associated with each talk is necessarily temporal. The work presented here may be in a state of flux. In all cases, please consult the authors' Web pages for up-to-date information. Please don't refer to these pages as a definitive source. Design and Research Paul Graham What happens when you treat programming languages as a design problem instead of a research topic? What do you do differently when building a programming language is like designing a chair, or a building, or a new typeface? Ultimately I think research and design converge. If so, for programming language researchers, this talk will be a description of what the target looks like from the back. Serving the Web Paul Graunke (Northeastern University), Robert Bruce Findler (University of Chicago), Shriram Krishnamurthi (Brown University), Matthias Felleisen (Northeastern University) The Web, originally designed for static content, now contains large amounts of dynamically generated content. The increase in flexibility afforded by Web browsers strains most methods of constructing Web software, leading to many defects. In order to understand and address these defects, we construct a model of the Web. Our model captures several kinds of defects. First, Web programs interact with each other through Web forms. Current Web systems fail to prevent programs from attempting to extract non-existent fields from Web forms. Second, the nature of the HTTP protocol interferes with updating pages once sent to the client. These outdated pages lead consumers to make misinformed decisions which the server interprets in the context of an incompatible state, leading to disaster. My talk will also present an overview of all of our Web development tools, the shortcomings exposed by our model, and how we address them Rigorously Modelling and Analyzing Hybrid Systems using Analytic Constraint Logic Programming Tim Hickey (Brandeis University) We use an interval-based Analytic Constraint Logic Programming (ACLP) language to accurately and declaratively model highly non-linear ODE-based Hybrid Systems. The use of ACLP allows one to introduce variables representing real valued functions and to constrain them using functional equations. This provides a rigorous and declarative model for Hybrid systems in which the behavior of the ACLP program precisely mirrors the (theoretical) behavior of the Hybrid system. One potential advantage of this approach is that program analysis tools developed to analyze ACLP programs should automatically provide tools for analyzing Hybrid systems. In this talk we describe the ACLP framework, demonstrate how it can be used to model Hybrid systems, and discuss the correspondence between program analysis tools and Hybrid system analysis tools. DrJVM: Safe, Efficient Support for Dynamic Class Upgrades in Java David Reiss, Gregory Cooper, and Shriram Krishnamurthi (Brown University) Software systems often require upgrades, both to fix bugs and to add new features. Upgrades traditionally consist of new libraries and executables, which take effect only after the user restarts the system. In some applications, however, shutting a system down is infeasible, and in such cases, users require the ability to upgrade code within a running system. While researchers have investigated ways of implementing this capability, existing work suffers from various weaknesses, including loss of static type safety, inconvenience to the programmer, or performance degradation. In this talk, we present DrJVM, an implementation of the Java Virtual Machine that supports dynamic upgrades in a type-safe, convenient, and efficient manner. Report on a Five Year Experiment in Teaching Web Programming in Scheme as a Computer Literacy Course Tim Hickey (Brandeis University) In this talk I will describe our use of Jscheme (a dialect of Scheme implemented in Java) to teach the Computer Literacy course at Brandeis over the past five years and will argue that using Scheme to teach web programming allows one to be relevant in the student's eye's, while still managing to cover important concepts in computation. Language-Based Information-Flow Security Andrei Sabelfeld and Andrew Myers (Cornell University) Current standard security practices do not provide substantial assurance that the end-to-end behavior of a computing system satisfies important security policies such as confidentiality. An end-to-end confidentiality policy might assert that secret input data cannot be inferred by an attacker through the attacker's observations of system output; this policy regulates information flow. Conventional security mechanisms such as access control and encryption do not directly address the enforcement of information-flow policies. Recently, a promising new approach has been developed: the use of programming-language techniques for specifying and enforcing information-flow policies. This talk is intended to give the big picture of recent and current research on information-flow security, particularly focusing on work that uses static program analysis to enforce information-flow policies. Speaker's Supplement The talk is based on a recent survey article (to appear in IEEE J-SAC) written jointly with Andrew Myers, available via http://www.cs.cornell.edu/~andrei/Papers/jsac.ps. Implementing Staged Computation Chiyan Chen and Hongwei Xi (Boston University) Staged computation is a key to partial evaluation and run-time code generation. In this talk, we present a novel approach to implementing staged computation through the use of guarded recursive (g.r.) datatype constructors. We first show how the notion of code can be captured with g.r. datatype constructors and then present rules for typing and translating staged programs, written in the MetaML-like syntax, into ML-like programs that are typable in ML extended with g.r. datatype constructors (ML_gr). Compared to MetaML, our approach has the following advantages: 1. Staged programming can be completely embedded to ML_gr. As a consequence, we get free dynamic semantics for staged programming, as provided by ML_gr. Also, some difficult concepts in MetaML (e.g., the built-in functions such as "run" and "lift") are provided with a simple and natural explanation. Moreover, with our type-preserving translation, we also get free soundness (subject reduction) property of the typing for meta-ML style stage programming. 2. Our staged programming offers more expressiveness than MetaML: Some functions that are difficult or even impossible to stage in MetaML can be staged with our approach. 3. Our type system of staged programming is stronger than that of MetaML. In particular, we can readily differentiate open code from closed code, and thus can statically prevent open code from being executed. We also provide realistic examples in support of this simple and effective approach to staged computation, which can readily be made available in practice. Decomposing lambda: the Kernel programming language John N. Shutt (Worcester Polytechnic Institute) The Kernel programming language attempts to expand on the simplicity and versatility of Scheme by exploiting a decomposition of Scheme's lambda constructor into two orthogonal constructors. The primary constructor, called $vau, builds compound combiners that act directly on their unevaluated operands ("call-by-text"); while a second constructor, called simply "wrap", induces evaluation of arguments. This talk explains how these constructors work, and explores some of their consequences. Using the new constructors, a variety of core Scheme primitives may be constructed as Kernel compound combiners --- notably including $lambda, apply, $quote, and (incidentally) car and cdr. The capabilities of macro facilities are entirely subsumed. Kernel also incorporates several design differences from Scheme that help the programmer to manage the inherent volatility of first-class call-by-text compound combiners. Several past LISP languages have included devices similar to $vau (such as the notorious "FEXPRs") but did not offer sufficient means to manage the accompanying volatility. The talk describes several of Kernel's management-motivated deviations from Scheme, ranging from overt syntax to subtle semantics. Computational Soundness of Non-Confluent Calculi Elena Machkasova (Wellesley College) Traditionally, there are two ways of reasoning about a program: a small step operational semantics that defines the meaning of a program and a calculus rewrite relation that describes program transformations. Computational soundness connects these two; it implies that any transformation expressible in the calculus preserves meaning with respect to the small-step operational semantics. The usual technique for proving computational soundness is based on confluence and standardization. However, this approach is not applicable to many calculi because of lack of confluence. In this talk I will give a brief overview of the traditional approach to computational soundness proofs and describe a technique for proving computational soundness which does not require confluence of the calculus. The technique is based on two properties, lift and project, introduced in Machkasova and Turbak ``A Calculus for Link-time Compilation''. I will focus on a proof of these properties in the case of a small calculus of records with mutually recursive components. In addition to lacking confluence, this calculus does not have other properties commonly used in computational soundness proofs, such as left-linearity and finiteness of developments. However, we are able to show that the calculus is computationally sound. The MulSaw Approach to Automated Specification-Based Testing Darko Marinov and Sarfaz Khurshid (MIT) This talk presents two complementary frameworks that the MulSaw project has developed for automated specification-based testing of Java programs. Both frameworks test a method by first generating all nonisomorphic inputs (within a given input size) that satisfy the method precondition and then executing the method on each input and using the method postcondition as a test oracle for checking the correctness of each output. The first framework allows programmers to write specifications in Alloy, a first-order, relational language. This framework translates a precondition into a boolean satisfiability formula and uses an off-the-shelf SAT solver to enumerate solutions to the formula; these solutions correspond to nonisomorphic test inputs. The second framework allows programmers to write specifications using Java expressions. This framework provides a novel algorithm for generation of nonisomorphic inputs for which the Java predicate that corresponds to a precondition returns true. We have used these frameworks to test several Java programs, including data structure implementations from the Java Collections Framework, a naming architecture for mobile networks, and the Alloy Analyzer (AA). For data structures, the experimental results indicate that it is feasible to systematically generate inputs that achieve complete statement and branch coverage. For the naming architecture and AA, this systematic testing revealed subtle errors. Speaker's Supplement Details of the MulSaw project can be found online at http://mulsaw.lcs.mit.edu.

Last modified Friday, October 11th, 2002 1:31:59pm

Powered by