title: From SOS Rules to Proof Principles: An Operational Metatheory for Functional Languages

abstract: Structural Operational Semantics (SOS) is a widely used formalism for specifying the computational meaning of programs, and is commonly used in specifying the semantics of functional languages. Despite this widespread use there has been relatively little work on the for such semantics. As a consequence the operational approach to reasoning is considered ad hoc since the same basic proof techniques and reasoning tools are reestablished over and over, once for each operational semantics specification. This paper develops some metatheory for a certain class of SOS language specifications for functional languages. We define a rule format, Globally Deterministic SOS (GDSOS), and establish some proof principles for reasoning about equivalence which are sound for all languages which can be expressed in this format. More specifically, if the SOS rules for the operators of a language conform to the syntax of the GDSOS format, then - a syntactic analogy of continuity holds, which relates a recursive function to its finite unwindings, and forms the basis of a Scott-style fixed-point induction technique; - a powerful induction principle called improvement induction holds for a certain class of GDSOS semantics; the Improvement Theorem from [Sands, POPL'95] is a simple corollary; - a useful bisimulation-based coinductive proof technique for operational approximation (and its instrumented variants) is sound.


venue: popl

title: Constraints to Stop Higher-Order Deforestation

authors:
Helmut Seidl
Morten Heine Sørensen

abstract: Wadler's deforestation algorithm removes intermediate data structures from functional programs. To be appropriate for inclusion in a compiler, deforestation must terminate on all programs. Several techniques exist to ensure termination of deforestation on all first-order programs, but a technique for higher-order programs was only recently introduced by Hamilton and later Marlow. We present a new technique for ensuring termination of deforestation on all higher-order programs that allows useful transformation steps prohibited in Hamilton's and Marlow's techniques. The technique uses a constraint-based higher-order control-flow analysis. 1 Introduction Lazy, higher-order, functional programming languages lend themselves to a certain style of programming which uses intermediate data structures [28]. However, this style also leads to inefficient programs. Example 1 Consider the following program. letrec a = x; y: case x of [] ! y (h : t) ! h : a t y in u; v; w: a (a u v) w The mai...


title: Fast and Accurate Flow-Insensitive Points-To Analysis

authors:
Marc Shapiro
Susan Horwitz

abstract: In order to analyze a program that involves pointers, it is necessary to have (safe) information about what each pointer points to. There are many different approaches to computing points-to information. This paper addresses techniques for flow- and context-insensitive interprocedural analysis of stack-based storage.The paper makes two contributions to work in this area: - The first contribution is a set of experiments that explore the trade-offs between techniques previously defined by Lars Andersen and Bjarne Steensgaard. The former has a cubic worst-case running time, while the latter is essentially linear. However, the former may be much more precise than the latter. We have found that in practice, Andersen's algorithm is consistently more precise than Steensgaard's. For small programs, there is very little difference in the times required by the two approaches; however, for larger programs, Andersen's algorithm can be much slower than Steensgaard's. - The second contribution is the definition of two new algorithms. The first algorithm can be "tuned" so that its worst-case time and space requirements, as well as its accuracy range from those of Steensgaard to those of Andersen. We have experimented with several versions of this algorithm; one version provided a significant increase in accuracy over Steensgaard's algorithm, while keeping the running time within a factor of two. The second algorithm uses the first as a subroutine. Its worst-case time and space requirements are a factor of log N (where N is the number of variables in the program) worse than those of Steensgaard's algorithm. In practice, it appears to run about ten times slower than Steensgaard's algorithm; however it is significantly more accurate than Steensgaard's algorithm, and significantly faster than Andersen's algorithm on large programs.


title: Denotational Semantics Using an Operationally-Based Term Model

authors:
Mitchell Wand
Gregory T. Sullivan

abstract: We introduce a method for proving the correctness of transformations of programs in languages like Scheme and ML. The method consists of giving the programs a denotational semantics in an operationally-based term model in which interaction is the basic observable, and showing that the transformation is meaning-preserving. This allows us to consider correctness for programs that interact with their environment without terminating, and also for transformations that change the internal store behavior of the program. We illustrate the technique on one of the Meyer-Sieber examples, and we use it to prove the correctness of assignment elimination for Scheme. The latter is an important but subtle step for Scheme compilers; we believe ours is the first proof of its correctness.


title: Barrier Inference

authors:
Alexander Aiken
David Gay

abstract: Many parallel programs are written in SPMD style i.e. by running the same sequential program on all processes. SPMD programs include synchronization, but it is easy to write incorrect synchronization patterns. We propose a system that verifies a program's synchronization pattern. We also propose language features to make the synchronization pattern more explicit and easily checked. We have implemented a prototype of our system for Split-C and successfully verified the synchronization structure of realistic programs.


title: Correctness of Monadic State: An Imperative Call-by-Need Calculus

authors:
Zena M. Ariola
Amr Sabry

abstract: The extension of Haskell with a built-in state monad combines mathematical elegance with operational efficiency: -Semantically, at the source language level, constructs that act on the state are viewed as functions that pass an explicit store data structure around. -Operationally, at the implementation level, constructs that act on the state are viewed as statements whose evaluation has the side-effect of updating the implicit global store in place.There are several unproven conjectures that the two views are consistent.Recently, we have noted that the consistency of the two views is far from obvious: all it takes for the implementation to become unsound is one judiciously-placed beta-step in the optimization phase of the compiler. This discovery motivates the current paper in which we formalize and show the correctness of the implementation of monadic state.For the proof, we first design a typed call-by-need language that models the intermediate language of the compiler, together with a type-preserving compilation map. Second, we show that the compilation is semantics-preserving by proving that the compilation of every source axiom yields an observational equivalence of the target language. Because of the wide semantic gap between the source and target languages, we perform this last step using an additional intermediate language.The imperative call-by-need λ-Calculus is of independent interest for reasoning about system-level Haskell code providing services such as memo-functions, generation of new names, etc., and is the starting point for reasoning about the space usage of Haskell programs.


title: Parallel Beta Reduction is not Elementary Recursive

authors:
Andrea Asperti
Harry G. Mairson

abstract: We analyze the inherent complexity of implementing Lévy's notion of optimal evaluation for the &lambda-calculus, where similar redexes are contracted in one step via so-called parallel β-reduction. optimal evaluation was finally realized by Lamping, who introduced a beautiful graph reduction technology for sharing evaluation contexts dual to the sharing of values. His pioneering insights have been modified and improved in subsequent implementations of optimal reduction.We prove that the cost of parallel β-reduction is not bounded by any Kalmár-elementary recursive function. Not merely do we establish that the parallel β-step cannot, be a unit-cost operation, we demonstrate that the time complexity of implementing a sequence of n parallel β-steps is not bounded as O(2n), O(22n), O(222n), or in general, O(Kl(n)) where Kl(n) is a fixed stack of l 2s with an n on top.A key insight, essential to the establishment of this nonelementary lower bound, is that any simply-typed λ-term can be reduced to normal form in a number of parallel β-steps that is only polynomial in the length of the explicitly-typed term. The result follows from Statman's theorem that deciding equivalence of typed λ-terms is not elementary recursive.The main theorem gives a lower bound on the work that must be done by any technology that implements Lévy's notion of optimal reduction. However, in the significant case of Lamping's solution, we make some important remarks addressing how work done by β-reduction is translated into equivalent work carried out by his bookkeeping nodes. In particular, we identify the computational paradigms of superposition of values and of higher-order sharing, appealing to compelling analogies with quantum mechanics and SIMD-parallelism.


title: Edge Profiling versus Path Profiling: The Showdown

authors:
Thomas Ball
Peter Mataga
Shmuel Sagiv

abstract: Edge profiles are the traditional control flow profile of choice for profile-directed compilation. They have been the basis of path-based optimizations that select paths, even though edge profiles contain strictly less information than path profiles. Recent work on path profiling has suggested that path profiles are superior to edge profiles in practice.We present theoretic and algorithmic results that may be used to determine when an edge profile is a good predictor of hot paths (and what those hot paths are) and when it is a poor predictor. Our algorithms efficiently compute sets of definitely and potentially hot paths in a graph annotated with an edge profile. A definitely hot path has a frequency greater than some non-zero lower bound in all path profiles that induce a given edge profile.Experiments on the SPEC95 benchmarks show that a huge percentage of the execution frequency in these programs is dominated by definitely hot paths (on average, 84% for FORTRAN benchmarks and 76% for C benchmarks). We also show that various hot path selection algorithms based on edge profiles work extremely well in most cases, but that path profiling is needed in some cases. These results indicate the usefulness of our algorithms for characterizing edge profiles and selecting hot paths.


title: Maximal Static Expansion

authors:
Denis Barthou
Albert Cohen
Jean-Francois Collard

abstract: Memory expansions are classical means to extract parallelism from imperative programs. However, for dynamic control programs with general memory accesses, such transformations either fail or require some run-time mechanism to restore the data flow. This paper presents an expansion framework for any type of data structure in any imperative program, without the need for dynamic data flow restoration. The key idea is to group together the write operations that participate in the flow of the same datum. We show that such an expansion boils down to mapping each group to a single memory cell. We give a practical algorithm for code transformation. This algorithm, however, is valid for (possibly non-affine) loops over arrays only.


title: Escape Analysis: Correctness Proof, Implementation and Experimental Results

abstract: We describe an escape analysis [32, 14], used to determine whether the lifetime of data exceeds its static scope.We give a new correctness proof starting directly from a semantics. Contrary to previous proofs, it takes into account all the features of functional languages, including imperative features and polymorphism. The analysis has been designed so that it can be implemented under the small complexity bound of O(n log2 n) where n is the size of the analyzed program. We have included it in the Caml Special Light compiler (an implementation of ML), and applied it to very large programs. We plan to apply these techniques to the Java programming language.Escape analysis has been applied to stack allocation. We improve the optimization technique by determining minimal lifetime for stack allocated data, and using inlining. We manage to stack allocate 25% of data in the theorem prover Coq. We analyzed the effect of this optimization, and noticed that its main effect is to improve data locality, which is important for efficiency.


title: Path-Sensitive Value-Flow Analysis

authors:
Rastislav Bodík
Sadun Anik

abstract: When analyzing programs for value recomputation, one faces the problem of naming the value that flows between equivalent computations with different lexical names. This paper presents a data-flow analysis framework that overcomes this problem by synthesizing a name space tailored for tracing the values whose flow is of interest to a given data-flow problem. Furthermore, to exploit recomputation of a value with multiple, synonymous names, path-sensitive value numbering on the synthetic name space is developed. Optimizations that rely on value flow to detect redundant computations, such as partial redundancy elimination and constant propagation, become more powerful when phrased in our framework. The framework is built on a new program representation called Value Name Graph (VNG) which gains its power from integrating three orthogonal techniques: symbolic back-substitution, value numbering, and data-flow analysis. Our experiments with the implementation show that analysis on the VNG is p...


title: Manufacturing Cheap, Resilient, and Stealthy Opaque Constructs

authors:
Christian S. Collberg
Clark D. Thomborson
Douglas Low

abstract: It has become common to distribute software in forms that are isomorphic to the original source code. An important example is Java bytecode. Since such codes are easy to decompile, they increase the risk of malicious reverse engineering attacks.In this paper we describe the design of a Java code obfuscator, a tool which - through the application of code transformations - converts a Java program into an equivalent one that is more difficult to reverse engineer.We describe a number of transformations which obfuscate control-flow. Transformations are evaluated with respect to potency (To what degree is a human reader confused?), resilience (How well are automatic deobfuscation attacks resisted?), cost (How much time/space overhead is added?), and stealth (How well does obfuscated code blend in with the original code?).The resilience of many control-altering transformations rely on the resilience of opaque predicates. These are boolean valued expressions whose values are known to the obfuscator but difficult to determine for an automatic deobfuscator. We show how to construct resilient, cheap, and stealthy opaque predicates based on the intractability of certain static analysis problems such as alias analysis.


title: Fast Interprocedural Class Analysis

authors:
Greg DeFouw
David Grove
Craig Chambers

abstract: Previous algorithms for interprocedural control flow analysis of higher-order and/or object-oriented languages have been described that perform propagation or constraint satisfaction and take O(N3) time (such as Shivers's O-CFA and Heintze's set-based analysis), or unification and take O(Nα (N,N) time (such as Steensgaard's pointer analysis), or optimistic reachability analysis and take O(N) time (such as Bacon and Sweeney's Rapid Type Analysis). We describe a general parameterized analysis framework that integrates propagation-based and unification-based analysis primitives and optimistic reachability analysis, whose instances mimic these existing algorithms as well as several new algorithms taking O(N), O(Nα(N,N)), O(N2), and O(N2α(N,N)) time; our O(N) and O(Nα(N,N)) algorithms produce more precise results than the previous algorithms with these complexities. We implemented our algorithm framework in the Vortex optimizing compiler, and we measured the cost and benefit of these interprocedural analysis algorithms in practice on a collection of substantial Cecil and Java programs.


title: Alias Analysis of Executable Code

authors:
Saumya K. Debray
Robert Muth
Matthew Weippert

abstract: Recent years have seen increasing interest in systems that reason about and manipulate executable code. Such systems can generally benefit from information about aliasing. Unfortunately, most existing alias analyses are formulated in terms of high-level language features, and are unable to cope with features, such as pointer arithmetic, that pervade executable programs. This paper describes a simple algorithm that can be used to obtain aliasing information for executabie code. In order to be practical, the algorithm is carefut to keep its memory requirements low, sacrificing precision where necessary to achieve this goal. Experimental results indicate that it is nevertheless able to provide a reasonable amount of information about memory references across a variety of benchmark programs.


title: Classes and Mixins

authors:
Matthew Flatt
Shriram Krishnamurthi
Matthias Felleisen

abstract: While class-based object-oriented programming languages provide a flexible mechanism for re-using and managing related pieces of code, they typically lack linguistic facilities for specifying a uniform extension of many classes with one set of fields and methods. As a result, programmers are unable to express certain abstractions over classes.In this paper we develop a model of class-to-class functions that we refer to as mixins. A mixin function maps a class to an extended class by adding or overriding fields and methods. Programming with mixins is similar to programming with single inheritance classes, but mixins more directly encourage programming to interfaces.The paper develops these ideas within the context of Java. The results are 1. an intuitive model of an essential Java subset; 2. an extension that explains and models mixins; and 3. type soundness theorems for these languages.


title: Putting Pointer Analysis to Work

authors:
Rakesh Ghiya
Laurie J. Hendren

abstract: This paper addresses the problem of how to apply pointer analysis to a wide variety of compiler applications. We are not presenting a new pointer analysis. Rather, we focus on putting two existing pointer analyses, points-to analysis and connection analysis, to work.We demonstrate that the fundamental problem is that one must be able to compare the memory locations read/written via pointer indirections, at different program points, and one must also be able to summarize the effect of pointer references over regions in the program. It is straightforward to compute read/write sets for indirections involving stack-directed pointers using points-to information. However, for heap-directed pointers we show that one needs to introduce the notion of anchor handles into the connection analysis and then express read/write sets to the heap with respect to these anchor handles.Based on the read/write sets we show how to extend traditional analyses like common subexpression elimination, loop-invariant removal and location-invariant removal to include pointer references. We also demonstrate the use of our information on more advanced techniques such as array dependence testing and program understanding. We have implemented our techniques in our McCAT C compiler, and we demonstrate examples of applying our methods on a set of pointer-intensive C benchmarks, as well as present concrete empirical data on the improvements achieved.


title: Higher-Order unCurrying

authors:
John Hannan
Patrick Hicks

abstract: We present a formal specification of unCurrying for a higherorder, functional language with ML-style let-polymorphism. This specification supports the general unCurrying of functions, even for functions which are passed as arguments or returned as values. The specification also supports partial unCurrying of any consecutive parameters of a function, rather than only unCurrying all of a function's parameters. We present the specification as a deductive system which axiomatizes a judgment relating a source term with an unCurried form of the term. We prove that this system relates only typable terms and that it is correct with respect to an operational semantics. We define a practical algorithm, based on algorithm W, which implements the unCurrying and prove this algorithm sound and complete with respect to the deductive system. This algorithm generates maximally unCurried forms of source terms. These results provide a declarative framework for reasoning about unCurrying and support a richer form of unCurrying than is currently found in compilers for functional languages.


title: The SLam Calculus: Programming with Secrecy and Integrity

authors:
Nevin Heintze
Jon G. Riecke

abstract: The SLam calculus is a typed λ-calculus that maintains security information as well as type information. The type system propagates security information for each object in four forms: the object's creators and readers, and the object's indirect creators and readers (i.e., those agents who, through flow-of-control or the actions of other agents, can influence or be influenced by the content of the object). We prove that the type system prevents security violations and give some examples of its power.


title: Parallelization in Calculational Forms

authors:
Zhenjiang Hu
Masato Takeichi
Wei-Ngan Chin

abstract: The problems involved in developing efficient parallel programs have proved harder than those in developing efficient sequential ones, both for programmers and for compilers. Although program calculation has been found to be a promising way to solve these problems in the sequential world, we believe that it needs much more effort to study its effective use in the parallel world. In this paper, we propose a calculational framework for the derivation of efficient parallel programs with two main innovations:. -We propose a novel inductive synthesis lemma based on which an elementary but powerful parallelization theorem is developed. -We make the first attempt to construct a calculational algorithm for parallelization, deriving associative operators from data type definition and making full use of existing fusion and tupling calculations.Being more constructive, our method is not only helpful in the design of efficient parallel programs in general but also promising in the construction of parallelizing compiler. Several interesting examples are used for illustration.


title: Single and Loving It: Must-Alias Analysis for Higher-Order Languages

authors:
Suresh Jagannathan
Peter Thiemann
Stephen Weeks
Andrew K. Wright

abstract: In standard control-flow analyses for higher-order languages, a single abstract binding for a variable represents a set of exact bindings, and a single abstract reference cell represents a set of exact reference cells. While such analyses provide useful may-alias information, they are unable to answer mustalias questions about variables and cells, as these questions ask about equality of specific bindings and references.In this paper, we present a novel program analysis for higher-order languages that answers must-alias questions. At every program point, the analysis associates with each variable and abstract cell a cardinality, which is either single or multiple. If variable x is single at program point p, then all bindings for x in the heap reachable from the environment at p hold the same value. If abstract cell r is single at p, then at most one exact cell corresponding to r is reachable from the environment at p.Must-alias information facilitates various program optimizations such as lightweight closure conversion [19]. In addition, must-alias information permits analyses to perform strong updates [3] on abstract reference cells known to be single. Strong updates improve analysis precision for programs that make significant use of state.A prototype implementation of our analysis yields encouraging results. Over a range of benchmarks, our analysis classifies a large majority of the variables as single.


title: Inference of Polymorphic and Conditional Strictness Properties

abstract: 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 on polymorphic recursion whose soundness is established via a translation from the polymorphic system into the conjunctive system. From the polymorphic analysis, an inference algorithm based on constraint resolution is derived and shown complete for variant of the polymorphic analysis. The algorithm deduces at the same time a property and a set of hypotheses on the free variables of an expression which makes it suitable for analysis of program with module structure.


title: Bridging the Gulf: A Common Intermediate Language for ML and Haskell

authors:
Simon L. Peyton Jones
Mark Shields
John Launchbury
Andrew P. Tolmach

abstract: 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 infrastructure, and supporting language developments that move each language in the direction of the other. Achieving this goal without compromising the ability to Compile as good code as a more direct route turned out to be much more subtle than we expected. We address this challenge using monads and unpointed types, identify two alternative language designs, and explore the choices they embody.


title: Array SSA Form and Its Use in Parallelization

authors:
Kathleen Knobe
Vivek Sarkar

abstract: 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 for SSA form for arrays. The current SSA processing of arrays views an array as a single object. But the kinds of analyses that sophisticated compilers need to perform on arrays, for example those that drive loop parallelization, are at the element level. Current SSA form for arrays is incapable of providing the element-level data flow information required for such analyses.In this paper, we introduce an Array SSA form that captures precise element-level data flow information for array variables in all cases. It is general and simple, and coincides with standard SSA form when applied to scalar variables. It can also be used for structures and other variable types that can be modeled as arrays. An important application of Array SSA form is in automatic parallelization. We show how Array SSA form can enable parallelization of any loop that is free of loop-carried true data dependences. This includes loops with loop-carried anti and output dependences, unanalyzable subscript expressions, and arbitrary control flow within an iteration. Array SSA form achieves this level of generality by making manifest its - functions as runtime computations in cases that are not amenable to compile-time analysis.


title: Security Properties of Typed Applets

authors:
Xavier Leroy
François Rouaix

abstract: 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, such as procedural encapsulation, type abstraction, and systematic type-based placement of run-time checks. These results are a first step towards formal techniques for developing and validating safe execution environments for applets.


title: A Functional Representation of Data Structures with a Hole

abstract: 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 we present an approach to introducing data structures with a hole into call-by-value functional programming languages like ML. Data structures with a hole are formalized as a new form of λ-abstraction called hole abstraction. The novel features of hole abstraction are that expressions inside hole abstraction are evaluated and application is implemented by destructive update of a hole. We present a simply typed call-by-value λ-calculus extended with hole abstractions. Then we show a compilation method of hole abstraction and prove correctness of the compilation.


title: From System F to Typed Assembly Language

authors:
J. Gregory Morrisett
David Walker
Karl Crary
Neal Glew

abstract: 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 abstractions, such as closures, tuples, and objects, as well as user-defined abstract data types. The type system ensures that well-typed programs cannot violate these abstractions. In addition, the typing constructs place almost no restrictions on low-level optimizations such as register allocation, instruction selection, or instruction scheduling.Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly language provide a fully automatic way to produce proof carrying code, suitable for use in systems where untrusted and potentially malicious code must be checked for safety before execution.

awards: Most Influential POPL Paper (awarded 2008)


title: Javalight is Type-Safe - Definitely

authors:
Tobias Nipkow
David von Oheimb

abstract: 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 formally in the theorem prover Isabelle/HOL. Thus this paper demonstrates that machine-checking the design of non-trivial programming languages has become a reality.


title: Static Typing for Dynamic Messages

abstract: 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 needed for some programs, but it seems that there has been no proposal of static type systems for dynamic messages. This paper presents a static typing discipline for dynamic messages and formalizes it into a second order polymorphic type system. The type system satisfies the type soundness property and has a principal type inference algorithm. The type system therefore provides a foundation for a statically typed object-oriented language enriched with polymorphic dynamic messages.


title: From Polyvariant Flow Information to Intersection and Union Types

authors:
Jens Palsberg
Christina Pavlopoulou

abstract: 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 first formal relationship between polyvariant analysis and standard notions of type. In the spirit of Nielson and Nielson, we study a parameterized flow analysis which can be instantiated to the analyses of Agesen, Schmidt, and as a simple case also 0-CFA. Extended with safety checks, the flow analysis accepts and rejects programs, much like a type checker. We prove that if a program can be safety-checked by a finitary instantiation of the flow analysis, then it can also be typed in a type system with intersection types, union types, subtyping, and recursive types, but no universal or existential quantifiers. This provides a framework for designing and understanding combinations of flow analyses and type systems.


title: Local Type Inference

authors:
Benjamin C. Pierce
David N. Turner

abstract: 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 constraints such as unification variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound variables in function abstractions by propagating type constraints downward from enclosing application nodes. We motivate our design choices by a statistical analysis of the uses of type inference in a sizable body of existing ML code. 1 Introduction Most statically typed programming languages offer some form of type inference, allowing programmers to omit type annotations that can be recovered from context. Such a facility can eliminate a great deal of needless verbosity, making programs easier both to read and to write. Unfortunately, type infe...


title: A Typed Language for Distributed Mobile Processes (Extended Abstract)

authors:
James Riely
Matthew Hennessy

abstract: 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. Communication channels are explicitly located: the use of a channel requires knowledge of both the channel and its location. 2. Names are endowed with permissions: the holder of a name may only use that name in the manner allowed by these permissions.A type system is proposed in which-the types control the allocation of permissions; in well-typed processes all names are used in accordance with the permissions allowed by the types. We prove Subject Reduction and Type Safety Theorems for the type system. In the final section we define a semantic theory based on barbed bisimulations and discuss its characterization in terms of a bisimulation relation over a relativized labelled transition system.


title: Data Flow Analysis is Model Checking of Abstract Interpretations

abstract: 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 simplest possible terms that a d.f.a. is a model check of a program's a.i. trace. In particular, the classic flow equations for bit-vector-based d.f.a.s reformat trivially into modal mu-Calculus formulas. A surprising consequence is that two of the classical d.f.a.s are exposed as unsound; this problem is analyzed and simply repaired. In the process of making the above discoveries, we clarify the relationship between a.i. and d.f.a. in terms of the often-misunderstood notion of collecting semantics and we highlight how the research areas of flow analysis, abstract interpretation, and model checking have grown together.


title: Second-Order Unification and Type Inference for Church-Style Polymorphism

abstract: 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 contain variables. This requires another proof of the undecidability of the second-order unification since known results use variables in arguments of other variables. Moreover, our proof uses elementary techniques, which is important from the methodological point of view, because Goldfarb's proof [Gol81] highly relies on the undecidability of the tenth Hilbert's problem. 1 1 Introduction The Church-style system F was independently introduced by Girard [Gir72] and Reynolds [Rey74] as an extension of the simply-typed -calculus a type system introduced of H. B. Curry [Cur69]. As usual for type systems, the decidability of so called sequent decision problems was considered. A sequent decision problem in some ty...


title: Dynamic Typing as Staged Type Inference

authors:
Mark Shields
Tim Sheard
Simon L. Peyton Jones

abstract: 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 dynamic values, and can be syntactically awkward.We introduce a new approach to dynamic typing, based on staged computation, which allows a single type-reconstruction algorithm to execute partly at compile time and partly at run-time. This approach seamlessly extends a single type system to accommodate types that are only known at run-time, while still supporting both type inference and polymorphism. The system is significantly more expressive than other approaches. Furthermore it can be implemented efficiently; most of the type inference is done at compile-time, leaving only some residual unification for run-time.We demonstrate our approach by examples in a small polymorphic functional language, and present its type system, type reconstruction algorithm, and operational semantics. Our proposal could also be readily adapted to many other programming languages.


title: Secure Information Flow in a Multi-Threaded Imperative Language

authors:
Geoffrey Smith
Dennis M. Volpano

abstract: 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 variables. Here, we extend the analysis to deal with a multithreaded language. We show that the previous type system is insufficient to ensure a desirable security property called noninterference. Noninterference basically means that the final values of low variables are independent of the initial values of high variables. By modifying the sequential type system, we are able to guarantee noninterference for concurrent programs. Crucial to this result, however, is the use of purely nondeterministic thread scheduling. Since implementing such scheduling is problematic, we also show how a more restrictive type system can guarantee noninterference, given a more deterministic (and easily implementable) scheduling policy, such as round-robin time slicing. Finally, we consider the consequences of adding a clock to the language.


title: A Type System for Java Bytecode Subroutines

authors:
Raymie Stata
Martín Abadi

abstract: 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 bytecode verifier for security, its current descriptions are inadequate. This paper proposes using typing rules to describe the bytecode verifier because they are more precise than prose, clearer than code, and easier to reason about than either.JVML has a subroutine construct used for the compilation of Java's try-finally statement. Subroutines are a major source of complexity for the bytecode verifier because they are not obviously last-in/first-out and because they require a kind of polymorphism. Focusing on subroutines, we isolate an interesting, small subset of JVML. We give typing rules for this subset and prove their correctness. Our type system constitutes a sound basis for bytecode verification and a rational reconstruction of a delicate part of Sun's bytecode verifier.


title: A Core Calculus of Dependency

authors:
Martín Abadi
Anindya Banerjee
Nevin Heintze
Jon G. Riecke

abstract: Notions of program dependency arise in many settings: security, partial evaluation, program slicing, and call-tracking. We argue that there is a central notion of dependency common to these settings that can be captured within a single calculus, the Dependency Core Calculus (DCC), a small extension of Moggi's computational lambda calculus. To establish this thesis, we translate typed calculi for secure information flow, binding-time analysis, slicing, and call-tracking into DCC. The translations help clarify aspects of the source calculi. We also define a semantic model for DCC and use it to give simple proofs of noninterference results for each case.


title: Types for Mobile Ambients

authors:
Luca Cardelli
Andrew D. Gordon

abstract: Java has demonstrated the utility of type systems for mobile code, and in particular their use and implications for security. Security properties rest on the fact that a well-typed Java program (or the corresponding verified bytecode) cannot cause certain kinds of damage.In this paper we provide a type system for mobile computation, that is, for computation that is continuously active before and after movement. We show that a well-typed mobile computation cannot cause certain kinds of run-time fault: it cannot cause the exchange of values of the wrong kind, anywhere in a mobile system.


title: Relevant Context Inference

authors:
Ramkrishna Chatterjee
Barbara G. Ryder
William Landi

abstract: Relevant context inference (RCI) is a modular technique for flow- and context-sensitive data-flow analysis of statically typed object-oriented programming languages such as C++ and Java. RCI can be used to analyze complete programs as well as incomplete programs such as libraries; this approach does not require that the entire program be memory-resident during the analysis. RCI is presented in the context of points-to analysis for a realistic subset of C++. The empirical evidence obtained from a prototype implementation argues the effectiveness of RCI.


title: Software Watermarking: Models and Dynamic Embeddings

authors:
Christian S. Collberg
Clark D. Thomborson

abstract: Watermarking embeds a secret message into a cover message. In media watermarking the secret is usually a copyright notice and the cover a digital image. Watermarking an object discourages intellectual property theft, or when such theft has occurred, allows us to prove ownership.The Software Watermarking problem can be described as follows. Embed a structure W into a program P such that: W can be reliably located and extracted from P even after P has been subjected to code transformations such as translation, optimization and obfuscation; W is stealthy; W has a high data rate; embedding W into P does not adversely affect the performance of P; and W has a mathematical property that allows us to argue that its presence in P is the result of deliberate actions.In the first part of the paper we construct an informal taxonomy of software watermarking techniques. In the second part we formalize these results. Finally, we propose a new software watermarking technique in which a dynamic graphic watermark is stored in the execution state of a program.


title: Typed Memory Management in a Calculus of Capabilities

authors:
Karl Crary
David Walker
J. Gregory Morrisett

abstract: Abstract An increasing number of systems rely on programming language technology to ensure safety and security of low-level code. Unfortunately, these systems typically rely on a complex, trusted garbage collector. Region-based type systems provide an alternative to garbage collection by making memory management explicit but verifiably safe. However, it has not been clear how to use regions in low-level, type-safe code. We present a compiler intermediate language, called the Capability Calculus, that supports region-based memory management, enjoys a provably safe type system, and is straightforward to compile to a typed assembly language. Source languages may be compiled to our language using known region inference algorithms. Furthermore, region lifetimes need not be lexically scoped in our language, yet the language may be checked for safety without complex analyses. Finally, our soundness proof is relatively simple, employing only standard techniques.


title: AnnoDomini: From Type Theory to Year 2000 Conversion Tool

authors:
Peter Harry Eidorff
Fritz Henglein
Christian Mossin
Henning Niss
Morten Heine Sørensen
Mads Tofte

abstract: AnnoDomini is a source-to-source conversion tool for making COBOL programs Year 2000 compliant. It is technically and conceptually built upon type-theoretic techniques and methods: type-based specification, program analysis by type inference and type-directed transformation. These are combined into an integrated software reengineering tool and method for finding and fixing Year 2000 problems. AnnoDomini's primary goals have been flexibility (support for multiple year representations), completeness (identifying all potential Year 2000 problems), correctness (correct fixes for Year 2000 problems) and a high degree of safe automation in all phases (declarative specification of conversions, no second-guessing or dangerous heuristics).In this paper we present the type-theoretic foundations of AnnoDomini: type system, type inference, unification theory, semantic soundness, and correctness of conversion. We also describe how these foundations have been applied and extended to a common COBOL mainframe dialect, and how AnnoDomini is packaged with graphical user interface and syntax-sensitive editor into a commercially available software tool.


title: Optimal Code Selection in DAGs

abstract: We extend the tree parsing approach to code selection to DAGs. In general, our extension does not produce the optimal code selection for all DAGs (this problem would be NPcomplete) , but for certain code selection grammars, it does. We present a method for checking whether a code selection grammar belongs to this set of DAG-optimal grammars, and use this method to check code selection grammars adapted from lcc: the grammars for the MIPS and SPARC architectures are DAG-optimal, and the code selection grammar for the 386 architecture is almost DAG-optimal.


title: Representing Layered Monads

abstract: There has already been considerable research on constructing modular, monad-based specifications of computational effects (state, exceptions, nondeterminism, etc.) in programming languages. We present a simple framework in this tradition, based on a Church-style effect-typing system for an ML-like language. The semantics of this language is formally defined by a series of monadic translations, each one expanding away a layer of effects. Such a layered specification is easy to reason about, but its direct implementation (whether by parameterized interpretation or by actual translation) is often prohibitively inefficient.By exploiting deeper semantic properties of monads, however, it is also possible to derive a vastly more efficient implementation: we show that each layer of effects can be uniformly simulated by continuation-passing, and further that multiple such layers can themselves be simulated by a standard semantics for call/cc and mutable state. Thus, even multi-effect programs can be executed in Scheme or SML/NJ at full native speed, generalizing an earlier single-effect result. As an example, we show how a simple resumption-based semantics of concurrency allows us to directly simulate a shared-state program across all possible dynamic interleavings of execution threads.


title: Type-Safe Linking and Modular Assembly Language

authors:
Neal Glew
J. Gregory Morrisett

abstract: Linking is a low-level task that is usually vaguely specified, if at all, by language definitions. However, the security of web browsers and other extensible systems depends crucially upon a set of checks that must be performed at link time. Building upon the simple, but elegant ideas of Cardelli, and module constructs from high-level languages, we present a formal model of typed object files and a set of inference rules that are sufficient to guarantee that type safety is preserved by the linking process.\n\nWhereas Cardelli's link calculus is built on top of the simply-typed lambda calculus, our object files are based upon typed assembly language so that we may model important low-level implementation issues. Furthermore, unlike Cardelli, we provide support for abstract types and higher-order type constructors - features critical for building extensible systems or modern programming languages such as ML.


title: Stochastic Processes as Concurrent Constraint Programs

abstract: ) Vineet Gupta Radha Jagadeesan Prakash Panangaden y vgupta@mail.arc.nasa.gov radha@cs.luc.edu prakash@cs.mcgill.ca Caelum Research Corporation Dept. of Math. and Computer Sciences School of Computer Science NASA Ames Research Center Loyola University--Lake Shore Campus McGill University Moffett Field CA 94035, USA Chicago IL 60626, USA Montreal, Quebec, Canada Abstract This paper describes a stochastic concurrent constraint language for the description and programming of concurrent probabilistic systems. The language can be viewed both as a calculus for describing and reasoning about stochastic processes and as an executable language for simulating stochastic processes. In this language programs encode probability distributions over (potentially infinite) sets of objects. We illustrate the subtleties that arise from the interaction of constraints, random choice and recursion. We describe operational semantics of these programs (programs are run by sampling random choices), deno...


title: Principality and Decidable Type Inference for Finite-Rank Intersection Types

authors:
A. J. Kfoury
J. B. Wells

abstract: Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable α-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. This is also in contrast to earlier presentations of intersection types where the status (decidable or undecidable) of these properties is unknown for the finite-rank restrictions at 3 and above. Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (without rank restrictions). In our system the earlier notion of expansion is integrated in the form of expansion variables, which are subject to substitution as are ordinary variables. A unification-based type inference algorithm is presented using a new form of unification, β-unification.


title: Quasi-Linear Types

abstract: Linear types (types of values that can be used just once) have been drawing a great deal of attention because they are useful for memory management, in-place update of data structures, etc.: an obvious advantage is that a value of a linear type can be immediately deallocated after being used. However, the linear types have not been applied so widely in practice, probably because linear values (values of linear types) in the traditional sense do not so often appear in actual programs. In order to increase the applicability of linear types, we relax the condition of linearity by extending the types with information on an evaluation order and simple dataflow information. The extended type system, called a quasi-linear type system, is formalized and its correctness is proved. We have implemented a prototype type inference system for the core-ML that can automatically find out which value is linear in the relaxed sense. Promising results were obtained from preliminary experiments with the prototype system.


title: Improvement in a Lazy Context: An Operational Theory for Call-by-Need

authors:
Andrew Moran
David Sands

abstract: The standard implementation technique for lazy functional languages is call-by-need, which ensures that an argument to a function in any given call is evaluated at most once. A significant problem with call-by-need is that it is difficult -- even for compiler writers -- to predict the effects of program transformations. The traditional theories for lazy functional languages are based on call-by-name models, and offer no help in determining which transformations do indeed optimize a program.In this article we present an operational theory for call-by-need, based upon an improvement ordering on programs: M is improved by N if in all program-contexts C, when C[M] terminates then C[N] terminates at least as cheaply.We show that this improvement relation satisfies a "context lemma", and supports a rich inequational theory, subsuming the call-by-need lambda calculi of Ariola et al. [AFM+95]. The reduction-based call-by-need calculi are inadequate as a theory of lazy-program transformation since they only permit transformations which speed up programs by at most a constant factor (a claim we substantiate); we go beyond the various reduction-based calculi for call-by-need by providing powerful proof rules for recursion, including syntactic continuity -- the basis of fixed-point-induction style reasoning, and an improvement theorem, suitable for arguing the correctness and safety of recursion-based program transformations.


title: JFlow: Practical Mostly-Static Information Flow Control

abstract: A promising technique for protecting privacy and integrity of sensitive data is to statically check information flow within programs that manipulate the data. While previous work has proposed programming language extensions to allow this static checking, the resulting languages are too restrictive for practical use and have not been implemented. In this paper, we describe the new language JFlow, an extension to the Java language that adds statically-checked information flow annotations. JFlow provides several new features that make information flow checking more flexible and convenient than in previous models: a decentralized label model, label polymorphism, run-time label checking, and automatic label inference. JFlow also supports many language features that have never been integrated successfully with static information flow control, including objects, subclassing, dynamic type tests, access control, and exceptions. This paper defines the JFlow language and presents formal rules that are used to check JFlow programs for correctness. Because most checking is static, there is little code space, data space, or run-time overhead in the JFlow implementation.

awards: Most Influential POPL Paper (awarded 2009)


title: A Simple, Comprehensive Type System for Java Bytecode Subroutines

abstract: A type system with proven soundness is a prerequisite for the safe and efficient execution of Java bytecode programs. So far, efforts to construct such a type system have followed a forward dataflow approach, in the spirit of the original Java Virtual Machine bytecode verifier. We present an alternative type system, based on conventional ideas of type constraints, polymorphic recursion and continuations. We compare it to Stata and Abadi's JVML-0 type system for bytecode subroutines, and demonstrate that our system is simpler and able to type strictly more programs, including code that could be produced by Java compilers and cannot be typed in JVML-0. Examination of real Java programs shows that such code is rare but does occur. We explain some of the apparently arbitrary constraints imposed by previous approaches by showing that they are consequences of our simpler type rules, or actually unnecessary.


title: Type-Based Analysis of Uncaught Exceptions

authors:
François Pessaux
Xavier Leroy

abstract: This paper presents a program analysis to estimate uncaught exceptions in ML programs. This analysis relies on unification-based type inference in a non-standard type system, using rows to approximate both the flow of escaping exceptions (a la effect systems) and the flow of result values (a la control-flow analyses). The resulting analysis is efficient and precise; in particular, arguments carried by exceptions are accurately handled.


title: Aggregate Structure Identification and Its Application to Program Analysis

authors:
G. Ramalingam
John Field
Frank Tip

abstract: In this paper, we describe an efficient algorithm for lazily decomposing aggregates such as records and arrays into simpler components based on the access patterns specific to a given program. This process allows us both to identify implicit aggregate structure not evident from declarative information in the program, and to simplify the representation of declared aggregates when references are made only to a subset of their components. We show that the structure identification process can be exploited to yield the following principal results: - A fast type analysis algorithm applicable to program maintenance applications such as date usage inference for the "Year 2000" problem. - An efficient algorithm for atomization of aggregates. Given a program, an aggregate atomization decomposes all of the data that can be manipulated by the program into a set of disjoint atoms such that each data reference can be modeled as one or more references to atoms without loss of semantic information. Aggregate atomization can be used to adapt program analyses and representations designed for scalar data to aggregate data. In particular, atomization can be used to build more precise versions of program representations such as SSA form or PDGs. Such representations can in turn yield more accurate results for problems such as program slicing.Our techniques are especially useful in weakly-typed languages such as Cobol (where a variable need not be declared as an aggregate to store an aggregate value) and in languages where references to statically-defined subranges of data such as arrays or strings are allowed.


title: Trust and Partial Typing in Open Systems of Mobile Agents

abstract: We present a partially-typed semantics for Dπ, a distributed π-calculus. The semantics is designed for mobile agents in open distributed systems in which some sites may harbor malicious intentions. Nonetheless, the semantics guarantees traditional type-safety properties at "good" locations by using a mixture of static and dynamic type-checking. We show how the semantics can be extended to allow trust between sites, improving performance and expressiveness without compromising type-safety.


title: Continuous Grammars

abstract: After defining appropriate metrics on strings and parse trees, the classic definition of continuity is adapted and applied to functions from strings to parse trees. Grammars that yield continuous mappings are of special interest, because they provide a sound theoretical framework for syntax error correction. Continuity justifies the approach, taken by many error correctors, to use the function output (the parse tree), and all the additional information it provides, in order to find corrections to the function input (the string). We prove that all Bounded Context grammars are continuous and that all continuous grammars are Bounded Context Parseable grammars, giving a characterization of continuous grammars in terms of possible parsing algorithms.


title: Parametric Shape Analysis via 3-Valued Logic

authors:
Shmuel Sagiv
Thomas W. Reps
Reinhard Wilhelm

abstract: We present a family of abstract-interpretation algorithms that are capable of determining "shape invariants" of programs that perform destructive updating on dynamically allocated storage. The main idea is to represent the stores that can possibly arise during execution using three-valued logical structures.


title: Extending the Scope of Syntactic Abstraction

authors:
Oscar Waddell
R. Kent Dybvig

abstract: The benefits of module systems and lexically scoped syntactic abstraction (macro) facilities are well-established in the literature. This paper presents a system that seamlessly integrates modules and lexically scoped macros. The system is fully static, permits mutually recursive modules, and supports separate compilation. We show that more dynamic module facilities are easily implemented at the source level in the extended language supported by the system.


title: Constraint Systems for Useless Variable Elimination

authors:
Mitchell Wand
Igor Siveroni

abstract: A useless variable is one whose value contributes nothing to the final outcome of a computation. Such variables are unlikely to occur in human-produced code, but may be introduced by various program transformations. We would like to eliminate useless parameters from procedures and eliminate the corresponding actual parameters from their call sites. This transformation is the extension to higher-order programming of a variety of dead-code elimination optimizations that are important in compilers for first-order imperative languages.


title: Once Upon a Polymorphic Type

authors:
Keith Wansbrough
Simon L. Peyton Jones

abstract: We present a sound type-based `usage analysis' for a realistic lazy functional language. Accurate information on the usage of program subexpressions in a lazy functional language permits a compiler to perform a number of useful optimisations. However, existing analyses are either ad-hoc and approximate, or defined over restricted languages. Our work extends the Once Upon A Type system of Turner, Mossin, and Wadler (FPCA'95). Firstly, we add type polymorphism, an essential feature of typed functional programming languages. Secondly, we include general Haskell-style user-defined algebraic data types. Thirdly, we explain and solve the `poisoning problem', which causes the earlier analysis to yield poor results. Interesting design choices turn up in each of these areas. Our analysis is sound with respect to a Launchbury-style operational semantics, and it is straightforward to implement. Good results have been obtained from a prototype implementation, and we are currently integrating the system into the Glasgow Haskell Compiler.


title: Dependent Types in Practical Programming

authors:
Hongwei Xi
Frank Pfenning

abstract: We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML(C) language schema. This allows specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. A major complication resulting from introducing dependent types is that pure type inference for the enriched system is no longer possible, but we show that type-checking a sufficiently annotated program in DML(C) can be reduced to constraint satisfaction in the constraint domain C. We exhibit the unobtrusiveness of our approach through practical examples and prove that DML(C) is conservative over ML. The main contribution of the paper lies in our language design, including the formulation of type-checking rules which makes the approach practical. To our knowledge, no previous type system for a general purpose programming language such as ML has combined dependent types with features including datatype declarations, higher-order functions, general recursions, let-polymorphism, mutable references, and exceptions. In addition, we have finished a prototype implementation of DML(C) for an integer constraint domain C, where constraints are linear inequalities (Xi and Pfenning 1998).


title: A Compositional Account of the Java Virtual Machine

abstract: The Java Virtual Machine (or JVM) is central to the system's aim of providing a secure program execution environment that operates identically on a wide variety of computing platforms. To be most effective in this role, the JVM needs a rigorous, complete description, to specify precisely the behavior required of implementations. In response, a number of researchers have produced formal accounts of the JVM that seek to define it in an unambiguous and comprehensible manner. Unfortunately, the size and complexity of the JVM means that many of these formal accounts must either restrict their scope substantially, or risk becoming unwieldy and intractable. This paper suggests an alternative approach to the specification of the JVM that seeks to ameliorate such problems by composing together a small set of "microinstructions" to produce the full bytecode set. These microinstructions are encapsulated as functions in the polymorphic functional programming language Haskell, using the familiar mechanisms of Hindley-Milner type inference to characterize the JVM's rather thorny verifier. In this way, its is hoped that a foundation will be laid for formal descriptions of the Java Virtual Machine that need not trade tractability for completeness.


title: Authentication Primitives and Their Compilation

authors:
Martín Abadi
Cédric Fournet
Georges Gonthier

abstract: Adopting a programming-language perspective, we study the problem of implementing authentication in a distributed system. We define a process calculus with constructs for authentication and show how this calculus can be translated to a lower-level language using marshaling, multiplexing, and cryptographic protocols. Authentication serves for identitybased security in the source language and enables simplifications in the translation. We reason about correctness relying on the concepts of observational equivalence and full abstraction.


title: Transforming Out Timing Leaks

abstract: One aspect of security in mobile code is privacy: private (or secret) data should not be leaked to unauthorised agents. Most of the work on secure information flow has until recently only been concerned with detecting direct and indirect flows. Secret information can however be leaked to the attacker also through covert channels. It is very reasonable to assume that the attacker, even as an external observer, can monitor the timing (including termination) behaviour of the program. Thus to claim a program secure, the security analysis must take also these into account.


title: Modular Refinement of Hierarchic Reactive Machines

authors:
Rajeev Alur
Radu Grosu

abstract: Scalable formal analysis of reactive programs demands integration of modular reasoning techniques with existing analysis tools. Principles such as abstraction, compositional refinement, and assume-guarantee reasoning are well understood for architectural hierarchy that describes the communication structure between component processes, and have been shown to be useful. In this paper, we develop the theory of modular reasoning for behavior hierarchy that describes control structure using hierarchic modes. From STATECHARTS to UML, behavior hierarchy has been an integral component of many software design languages, but only syntactically. We present the hierarchic reactive modules language that retains powerful features such as nested modes, mode reuse, exceptions, group transitions, history, and conjunctive modes, and yet has a semantic notion of mode hierarchy. We present an observational trace semantics for modes that provides the basis for mode refinement. We show the refinement to be compositional with respect to the mode constructors, and develop an assume-guarantee reasoning principle.


title: A Semantic Model of Types and Machine Instructions for Proof-Carrying Code

authors:
Andrew W. Appel
Amy P. Felty

abstract: Proof-carrying code is a framework for proving the safety of machine-language programs with a machinecheckable proof. Such proofs have previously defined type-checking rules as part of the logic. We show a universal type framework for proof-carrying code that will allow a code producer to choose a programming language, prove the type rules for that language as lemmas in higher-order logic, then use those lemmas to prove the safety of a particular program. We show how to handle traversal, allocation, and initialization of values in a wide variety of types, including functions, records, unions, existentials, and covariant recursive types. 1 Introduction When a host computer runs an untrusted program, the host may want some assurance that the program does no harm: does not access unauthorized resources, read private data, or overwrite valuable data. Proof-carrying code [Nec97] is a technique for providing such assurances. With PCC, the host -- called the "code consumer" -- specifies a sa...


title: (Optimal) Duplication is not Elementary Recursive

authors:
Andrea Asperti
Paolo Coppola
Simone Martini

abstract: In 1998 Asperti and Mairson proved that the cost of reducing a lambda-term using an optimal lambda-reducer (a la Lévy) cannot be bound by any elementary function in the number of shared-beta steps. We prove in this paper that an analogous result holds for Lamping’s abstract algorithm. That is, there is no elementary function in the number of shared beta steps bounding the number of duplication steps of the optimal reducer. This theorem vindicates the oracle of Lamping’s algorithm as the culprit for the negative result of Asperti and Mairson. The result is obtained using as a technical tool Elementary Affine Logic. Key words: complexity, elementary affine logic, graph rewriting, optimal reduction


title: First-Class Macros have Types

abstract: In modern Scheme, a macro captures the lexical environment where it is defined. This creates an opportunity for extending Scheme so that macros are first-class values. The key to achieving this goal, while preserving the ability to compile programs into reasonable code, is the addition of a type system. Many interesting things can be done with first-class macros, including the construction of a useful module system in which modules are also first-class. Clams got legs! — B.C.


title: Anytime, Anywhere: Modal Logics for Mobile Ambients

authors:
Luca Cardelli
Andrew D. Gordon

abstract: The Ambient Calculus is a process calculus where processes may reside within a hierarchy of locations and modify it. The purpose of the calculus is to study mobility, which is seen as the change of spatial configurations over time. In order to describe properties of mobile computations we devise a modal logic that can talk about space as well as time, and that has the Ambient Calculus as a model.

awards: Most Influential POPL Paper (awarded 2010)


title: A Debate on Language and Tool Support for Design Patterns

authors:
Craig Chambers
Bill Harrison
John M. Vlissides

abstract: Design patterns have earned a place in the developer's arsenal of tools and techniques for software development. They have proved so useful, in fact, that some have called for their promotion to programming language features. In turn this has rekindled the age-old debate over the mechanism that belong in programming languages versus those that are better served by tools. The debate comes full circle when one contemplates code generation and methodological tool support for patterns. The authors compare and contrast programming languages, tools, and patterns to assess their relative merits and to clarify their roles in the development process.


title: Paths vs. Trees in Set-Based Program Analysis

authors:
Witold Charatonik
Andreas Podelski
Jean-Marc Talbot

abstract: Set-based analysis of logic programs provides an accurate method for descriptive type-checking of logic programs. The key idea of this method is to upper approximate the least model of the program by a regular set of trees. In 1991, Frühwirth, Shapiro, Vardi and Yardeni raised the question whether it can be more efficient to use the domain of sets of paths instead, i.e., to approximate the least model by a regular set of words. We answer the question negatively by showing that type-checking for path-based analysis is as hard as the set-based one, that is DEXPTIME-complete. This result has consequences also in the areas of set constraints, automata theory and model checking.


title: Reducing Sweep Time for a Nearly Empty Heap

authors:
Yoo C. Chung
Soo-Mook Moon
Kemal Ebcioglu
Dan Sahlin

abstract: Mark and sweep garbage collectors are known for using time proportional to the heap size when sweeping memory, since all objects in the heap, regardless of whether they are live or not, must be visited in order to reclaim the memory occupied by dead objects. This paper introduces a sweeping method which traverses only the live objects, so that sweeping can be done in time dependent only on the number of live objects in the heap.


title: Enforcing Trace Properties by Program Transformation

authors:
Thomas Colcombet
Pascal Fradet

abstract: We propose an automatic method to enforce trace properties on programs. The programmer specifies the property separately from the program; a program transformer takes the program and the property and automatically produces another “equivalent” pogram satisfying the property. This separation of concerns makes the program easier to develop and maintain. Our approach is both static and dynamic. It integrates static analyses in order to avoid useless transformations. On the other hand, it never rejects programs but adds dynamic checks when necessary. An important challenge is to make this dynamic enforcement as inexpensive as possible. The most obvious application domain is the enforcement of security policies. In particular, a potential use of the method is the securization of mobile code upon receipt.


title: Temporal Abstract Interpretation

authors:
Patrick Cousot
Radhia Cousot

abstract: We study the abstract interpretation of temporal calculi and logics in a general syntax, semantics and abstraction independent setting. This is applied to the @@@@-calculus, a generalization of the μ-calculus with new reversal and abstraction modalities as well as a new time-symmetric trace-based semantics. The more classical set-based semantics is shown to be an abstract interpretation of the trace-based semantics which leads to the understanding of model-checking and its application to data-flow analysis as incomplete temporal abstract interpretations. Soundness and incompleteness of the abstractions are discussed. The sources of incompleteness, even for finite systems, are pointed out, which leads to the identification of relatively complete sublogics, à la CTL.


title: Resource Bound Certification

authors:
Karl Crary
Stephanie Weirich

abstract: Various code certification systems allow the certification and static verification of important safety properties such as memory and control-flow safety. These systems are valuable tools for verifying that untrusted and potentially malicious code is safe before execution. However, one important safety property that is not usually included is that programs adhere to specific bounds on resource consumption, such as running time.


title: Efficient Algorithms for pre* and post* on Interprocedural Parallel Flow Graphs

authors:
Javier Esparza
Andreas Podelski

abstract: This paper is a contribution to the already existing series of work on the algorithmic principles of interprocedural analysis. We consider the generalization to the case of parallel programs. We give algorithms that compute the sets of backward resp. forward reachable configurations for parallel flow graph systems in linear time in the size of the graph viz. the program. These operations are important in dataflow analysis and in model checking. In our method, we first model configurations as terms (viz. trees) in the process algebra PA that can express call stack operations and parallelism. We then give a 'declarative' Horn-clause specification of the sets of predecessors resp. successors. The 'operational' computation of these sets is carried out using the Dowling-Gallier procedure for HornSat.


title: Generalized Certificate Revocation

authors:
Carl A. Gunter
Trevor Jim

abstract: We introduce a language for creating and manipulating certificates, that is, digitally signed data based on public key cryptography, and a system for revoking certificates. Our approach provides a uniform mechanism for secure distribution of public key bindings, authorizations, and revocation information. An external language for the description of these and other forms of data is compiled into an intermediate language with a well-defined denotational and operational semantics. The internal language is used to carry out consistency checks for security, and optimizations for efficiency. Our primary contribution is a technique for treating revocation data dually to other sorts of information using a polarity discipline in the intermediate language.


title: A Framework for Combining Analysis and Verification

authors:
Nevin Heintze
Joxan Jaffar
Razvan Voicu

abstract: We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. Both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. More importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. In other words, our framework explores synergistic interaction between verification and analysis.


title: Analytic Constraint Solving and Interval Arithmetic

abstract: In this paper we describe the syntax, semantics, and implementation of the constraint logic programming language CLP(F) and we prove that the implementation is sound. A CLP(F) constraint is a conjunction of equations and inequations in a first order theory of analytic univariate functions over the reals. The theory allows vector-valued functions over closed intervals to be constrained in several ways, including specifying functional equations (possibly involving the differentiation operator) that must hold at each point in the domain, arithmetic constraints on the value of a function at a particular point in its domain, and bounds on the range of a function over its domain. After describing the syntax and semantics of the constraint language for CLP(F) and giving several examples, we show how to convert these analytic constraints into a subclass of simpler functional constraints which involve neither differentiation nor evaluation of functions. We then present an algorithm for solving these latter constraints and prove that it is sound. This implies the soundness of the CLP(F) interpreter. We also provide some timing results from an implementation of CLP(F) based on GNU Prolog. The current implementation is able to solve a wide variety of analytic constraints, but on particular classes of constraints (such as initial value problems for autonomous ODEs), it is not competitive with other non-constraint based, interval solvers such as Lohner's AWA system. CLP(F) should be viewed as a first step toward the long term goal of developing a practical, declarative, logic-based approach to numerical analysis.


title: A New Approach to Generic Functional Programming

abstract: This paper describes a new approach to generic functional programming, which allows us to define functions generically for all datatypes expressible in Haskell. A generic function is one that is defined by induction on the structure of types. Typical examples include pretty printers, parsers, and comparison functions. The advanced type system of Haskell presents a real challenge: datatypes may be parameterized not only by types but also by type constructors, type definitions may involve mutual recursion, and recursive calls of type constructors can be arbitrarily nested. We show that—despite this complexity—a generic function is uniquely defined by giving cases for primitive types and type constructors (such as disjoint unions and cartesian products). Given this information a generic function can be specialized to arbitrary Haskell datatypes. The key idea of the approach is to model types by terms of the simply typed λ-calculus augmented by a family of recursion operators. While conceptually simple, our approach places high demands on the type system: it requires polymorphic recursion, rank-n types, and a strong form of type constructor polymorphism. Finally, we point out connections to Haskell's class system and show that our approach generalizes type classes in some respects.


title: Type Elaboration and Subtype Completion for Java Bytecode

authors:
Todd B. Knoblock
Jakob Rehof

abstract: Java source code is strongly typed, but the translation from Java source to bytecode omits much of the type information originally contained within methods. Type elaboration is a technique for reconstructing strongly typed programs from incompletely typed bytecode by inferring types for local variables.


title: Semantics-Preserving Procedure Extraction

authors:
Raghavan Komondoor
Susan Horwitz

abstract: Procedure extraction is an important program transformation that can be used to make programs easier to understand and maintain, to facilitate code reuse, and to convert “monolithic” code to modular or object-oriented code. Procedure extraction involves the following steps:


title: Controlling Interference in Ambients

authors:
Francesca Levi
Davide Sangiorgi

abstract: Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences, which are similar to the interferences one finds in CCS and φ-calculus; and grave interferences, which are more dangerous and may be regarded as programming errors. To control interferences, the MA movement primitives are modified. On the new calculus, the Mobile Safe Ambients (SA), a type system is defined that: controls the mobility of ambients; removes all grave interferences. Other advantages of SA are: a useful algebraic theory; programs sometimes more robust (they require milder conditions for correctness) and/or simpler. These points are illustrated on several examples.


title: Implicit Parameters: Dynamic Scoping with Static Types

authors:
Jeffrey R. Lewis
John Launchbury
Erik Meijer
Mark Shields

abstract: This paper introduces a language feature, called implicit parameters, that provides dynamically scoped variables within a statically-typed Hindley-Milner framework. Implicit parameters are lexically distinct from regular identifiers, and are bound by a special with construct whose scope is dynamic, rather than static as with let. Implicit parameters are treated by the type system as parameters that are not explicitly declared, but are inferred from their use.


title: Type Systems for Distributed Data Structures

authors:
Ben Liblit
Alexander Aiken

abstract: Distributed-memory programs are often written using a global address space: any process can name any memory location on any processor. Some languages completely hide the distinction between local and remote memory, simplifying the programming model at some performance cost. Other languages give the programmer more explicit control, offering better potential performance but sacrificing both soundness and ease of use.


title: On the Complexity of Flow-Sensitive Dataflow Analyses

authors:
Robert Muth
Saumya K. Debray

abstract: This paper attempts to address the question of why certain dataflow analysis problems can be solved efficiently, but not others. We focus on flow-sensitive analyses, and give a simple and general result that shows that analyses that require the use of relational attributes for precision must be PSPACE-hard in general. We then show that if the language constructs are slightly strengthened to allow a computation to maintain a very limited summary of what happens along an execution path, inter-procedural analyses become EXPTIME-hard. We discuss applications of our results to a variety of analyses discussed in the literature. Our work elucidates the reasons behind the complexity results given by a number of authors, improves on a number of such complexity results, and exposes conceptual commonalities underlying such results that are not readily apparent otherwise.


title: Shape Analysis for Mobile Ambients

authors:
Hanne Riis Nielson
Flemming Nielson

abstract: The ambient calculus is a calculus of computation that allows active processes to move between sites. We present an analysis inspired by state-of-the-art pointer analyses that safety and accurately predicts which processes may turn up at what sites during the execution of a composite system. The analysis models sets of processes by sets of regular tree grammars enhanced with context-dependent counts, and it obtains its precision by combining a powerful redex materialisation with a strong redex reduction (in the manner of the strong updates performed in pointer analyses). The underlying ideas are flexible and scale up to general tree structures admitting powerful restructuring operations.


title: Sparse Code Motion

authors:
Oliver Rüthing
Jens Knoop
Bernhard Steffen

abstract: In this article, we add a third dimension to partial redundancy elimination by considering code size as a further optimization goal in addition to the more classical consideration of computation costs and register pressure. This results in a family of sparse code motion algorithms coming as modular extensions of the algorithms for busy and lazy code motion. Each of them optimally captures a predefined choice of priority between these three optimization goals, e.g. code size can be minimized while (1) guaranteeing at least the performance of the argument program, or (2) even computational optimality. Each of them can further be refined to simultaneously reduce the lifetimes of temporaries to a minimum. These algorithms are well-suited for size-critical application areas like smart cards and embedded systems, as they provide a handle to control the code replication problem of classical code motion techniques. In fact, we believe that our systematic, priority-based treatment of trade-offs between optimization goals may substantially decrease development costs of size-critical applications: users may “play” with the priorities until the algorithm automatically delivers a satisfactory solution.


title: A Type System for Dynamic Web Documents

authors:
Anders Sandholm
Michael I. Schwartzbach

abstract: Many interactive Web services use the CGI interface for communication with clients. They will dynamically create HTML documents that are presented to the client who then resumes the interaction by submitting data through incorporated form fields. This protocol is difficult to statically type-check if the dynamic documents are created by arbitrary script code using printf-like statements. Previous proposals have suggested using static document templates which trades flexibility for safety. We propose a notion of typed, higher-order templates that simultaneously achieve flexibility and safety. Our type system is based on a flow analysis of which we prove soundness. We present an efficient runtime implementation that respects the semantics of only well-typed programs. This work is fully implemented as part of the system for defining interactive Web services.


title: Deciding Type Equivalence with Singleton Kinds

authors:
Christopher A. Stone
Robert Harper

abstract: Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. Singletons are interesting because they provide a very general form of definitions for type variables, allow fine-grained control of type computations, and allow many equational constraints to be expressed within the type system.


title: Projection Merging: Reducing Redundancies in Inclusion Constraint Graphs

authors:
Zhendong Su
Manuel Fähndrich
Alexander Aiken

abstract: Inclusion-based program analyses are implemented by adding new edges to directed graphs. In most analyses, there are many different ways to add a transitive edge between two nodes, namely through each different path connecting the nodes. This path redundancy limits the scalability of these analyses. We present projection merging, a technique to reduce path redundancy. Combined with cycle elimination [7], projection merging achieves orders of magnitude speedup of analysis time on programs over that of using cycle elimination alone.


title: Verifying Secrets and Relative Secrecy

authors:
Dennis M. Volpano
Geoffrey Smith

abstract: Systems that authenticate a user based on a shared secret (such as a password or PIN) normally allow anyone to query whether the secret is a given value. For example, an ATM machine allows one to ask whether a string is the secret PIN of a (lost or stolen) ATM card. Yet such queries are prohibited in any model whose programs satisfy an information-flow property like Noninterference. But there is complexity-based justification for allowing these queries. A type system is given that provides the access control needed to prove that no well-typed program can leak secrets in polynomial time, or even leak them with nonnegligible probability if secrets are of sufficient length and randomly chosen. However, there are well-typed deterministic programs in a synchronous concurrent model capable of leaking secrets in linear time.


title: A Type System for Expressive Security Policies

abstract: Certified code is a general mechanism for enforcing security properties. In this paradigm, untrusted mobile code carries annotations that allow a host to verify its trustworthiness. Before running the agent, the host checks the annotations and proves that they imply the host's security policy. Despite the flexibility of this scheme, so far, compilers that generate certified code have focused on simple type safety properties rather than more general security properties.


title: Mobile values, new names, and secure communication

authors:
Martín Abadi
Cédric Fournet

abstract: We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols.


title: What packets may come: automata for network monitoring

authors:
Karthikeyan Bhargavan
Satish Chandra
Peter J. McCann
Carl A. Gunter

abstract: We consider the problem of monitoring an interactive device, such as an implementation of a network protocol, in order to check whether its execution is consistent with its specification. At rst glance, it appears that a monitor could simply follow the input-output trace of the device and check it against the specification. However, if the monitor is able to observe inputs and outputs only from a vantage point external to the device---as is typically the case---the problem becomes surprisingly difficult. This is because events may be bu ered, and even lost, between the monitor and the device, in which case, even for a correctly running device, the trace observed at the monitor could be inconsistent with the specification.In this paper, we formulate the problem of external monitoring as a language recognition problem. Given a specification that accepts a certain language of input-output sequences, we de ne another language that corresponds to input-output sequences observable externally. We also give an algorithm to check membership of a string in the derived language. It turns out that without any assumptions on the specification, this algorithm may take unbounded time and space. To address this problem, we de ne a series of properties of device specifications or protocols that can be exploited to construct e cient language recognizers at the monitor. We characterize these properties and provide complexity bounds for monitoring in each case.To illustrate our methodology, we describe properties of the Internet Transmission Control Protocol (TCP), and identify features of the protocol that make it challenging to monitor e ciently.


title: Secure safe ambients

authors:
Michele Bugliesi
Giuseppe Castagna

abstract: Secure Safe Ambients (SSA) are a typed variant of Safe Ambients [9], whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and implicit process and ambient behavior: process types account not only for immediate behavior, but also for the behavior resulting from capabilities a process acquires during its evolution in a given context. Based on that, the type system provides for static detection of security attacks such as Trojan Horses and other combinations of malicious agents.We study the type system of SSA, define algorithms for type checking and type reconstruction, define powerful languages for expressing security properties, and study a distributed version of SSA and its type system. For the latter, we show that distributed type checking ensures security even in ill-typed contexts, and discuss how it relates to the security architecture of the Java Virtual Machine.


title: Stratified operational semantics for safety and correctness of the region calculus

abstract: The region analysis of Tofte and Talpin is an attempt to determine statically the life span of dynamically allocated objects. But the calculus is at once intuitively simple, yet deceptively subtle, and previous theoretical analyses have been frustratingly complex: no analysis has revealed and explained in simple terms the connection between the subleties of the calculus and the imperative features it builds on. We present a novel approach for proving safety and correctness of a simplified version of the region calculus. We give a stratified operational semantics, composed of a highlevel semantics dealing with the conceptual difficulties of effect annotations, and a low-level one with explicit operations on a region-indexed store. The main results of the paper are a proof simpler than previous ones, and a modular approach to type safety and correctness. The flexibility of this approach is demonstrated by the simplicity of the extension to the full calculus with type and region polymorphism.


title: Avoiding exponential explosion: generating compact verification conditions

authors:
Cormac Flanagan
James B. Saxe

abstract: Current verification condition (VC) generation algorithms, such as weakest preconditions, yield a VC whose size may be exponential in the size of the code fragment being checked. This paper describes a two-stage VC generation algorithm that generates compact VCs whose size is worst-case quadratic in the size of the source fragment, and is close to linear in practice.This two-stage VC generation algorithm has been implemented as part of the Extended Static Checker for Java. It has allowed us to check large and complex methods that would otherwise be impossible to check due to time and space constraints.


title: Efficient deductive methods for program analysis

abstract: No abstract available.


title: Subtyping arithmetical types

abstract: We consider the type system formed by a finite set of primitive types such as integer, character, real, etc., and three type construction operators: (i) Cartesian product, (ii) disjoint sum, and (iii) recursive type definitions. Type equivalence is defined to obey the arithmetical rules: commutativity and associativity of product and sum and distributivity of product over sum. We offer a compact representation of the types in this system as multivariate algebraic functions. This type system admits two natural notions of subtyping: "multiplicative", which roughly corresponds to the notion of object-oriented subtyping, and "additive", which seems to be more appropriate in our context. Both kinds of subtyping can be efficiently computed if no recursive definitions are allowed. Our main result is that additive subtyping is undecidable in the general case. Perhaps surprisingly, this undecidability result is by reduction from Hilbert's Tenth Problem (HIO): the solution of Diophantine equations.