POPL

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. ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

Proof-carrying code is a framework for proving the safety of machine-language programs with a machine-checkable proof. Previous PCC frameworks have defined type-checking rules as part of the logic. We show a universal type framework for proof-carrying ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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, ...

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 ...

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 ...

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 ...

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 ...