7,482 papers · page 289 of 375
We define an inference system for modular strictness analysis of functional programs by extending a conjunctive strictness logic with polymorphic and conditional properties. This extended set of properties is used to define a syntax-directed, polymorphic strictness analysis based…
Compilers for ML and Haskell use intermediate languages that incorporate deeply-embedded assumptions about order of evaluation and side effects. We propose an intermediate language into which one can compile both ML and Haskell, thereby facilitating the sharing of ideas and infra…
Static single assignment (SSA) form for scalars has been a significant advance. It has simplified the way we think about scalar variables. It has simplified the design of some optimizations and has made other optimizations more effective. Unfortunately none of this can be be said…
This paper formalizes the folklore result that strongly-typed applets are more secure than untyped ones. We formulate and prove several security properties that all well-typed applets possess, and identify sufficient conditions for the applet execution environment to be safe, suc…
Data structures with a hole, in other words data structures with an uninitialized field, are useful to write efficient programs: they enable us to construct functional data structures flexibly and write functions such as append and map as tail recursive functions. In this paper w…
We motivate the design of a statically typed assembly language (TAL) and present a type-preserving translation from System F to TAL. The TAL we present is based on a conventional RISC assembly language, but its static type system provides support for enforcing high-level language…
Javalight is a large sequential sublanguage of Java. We formalize its abstract syntax, type system, well-formedness conditions, and an operational evaluation semantics. Based on this formalization, we can express and prove type soundness. All definitions and proofs have been done…
Dynamic messages are first-class messages dynamically bound to program variables. By dynamic messages, the methods to be invoked can be varied dynamically at run-time, which provides a powerful abstraction mechanism for object-oriented languages. Dynamic messages are critically n…
Many polyvariant program analyses have been studied in the 199Os, including k-CFA, poly-k-CFA, and the Cartesian product algorithm. The idea of polyvariance is to analyze functions more than once and thereby obtain better precision for each call site. In this paper we present the…
We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, without long-distance constrain…
We describe a foundational language for specifying dynamically evolving networks of distributed processes, Dπ. The language is a distributed extension of the π-calculus which incorporates the notions of remote execution, migration, and site failure. Novel features of Dπ include 1…
This expository paper simplifies and clarifies Steffen's depiction of data flow analysis (d.f.a.) as model checking: By employing abstract interpretation (a.i.) to generate program traces and by utilizing Kozen's modal mu-calculus to express trace properties, we express in simple…
We present a proof of the undecidability of type inference for the Church-style system F --- an abstraction of polymorphism. A natural reduction from the second-order unification problem to type inference leads to strong restriction on instances --- arguments of variables cannot …
Dynamic typing extends statically typed languages with a universal datatype, simplifying programs which must manipulate other programs as data, such as distributed, persistent, interpretive and generic programs. Current approaches, however, limit the use of polymorphism in dynami…
Previously, we developed a type system to ensure secure information flow in a sequential, imperative programming language [VSI96]. Program variables are classified as either high or low security; intuitively, we wish to prevent information from flowing from high variables to low …
Java is typically compiled into an intermediate language, JVML, that is interpreted by the Java Virtual Machine. Because mobile JVML code is not always trusted, a bytecode verifier enforces static constraints that prevent various dynamic errors. Given the importance of the byteco…
status: Published
This paper describes the development of the programming language Erlang during the period 1985-1997. Erlang is a concurrent programming language designed for programming large-scale distributed soft real-time control applications. The design of Erlang was heavily influenced by id…
An interprocedural flow analysis can justify inlining in higher-order languages. In principle, more inlining can be performed as analysis accuracy improves. This paper compares four flow analyses to determine how effectively they justify inlining in practice. The paper makes two …
We observe that the principal typing property of a type system is the enabling technology for modularity and separate compilation [10]. We use this technology to formulate a modular and polyvariant closure analysis, based on the rank 2 intersection types annotated with control-fl…