7,482 papers · page 277 of 375
Ben Liblit, Alexander Aiken
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…
Robert Muth, Saumya K. Debray
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 pr…
Hanne Riis Nielson, Flemming Nielson
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 compo…
Oliver Rüthing, Jens Knoop, Bernhard Steffen
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 algorithm…
Anders Sandholm, Michael I. Schwartzbach
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 sta…
Christopher A. Stone, Robert Harper
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 co…
Zhendong Su, Manuel Fähndrich, Alexander Aiken
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 scalabilit…
Dennis M. Volpano, Geoffrey Smith
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 quer…
David Walker
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 se…
María Alpuente, Michael Hanus, Salvador Lucas, Germán Vidal
Functional logic languages combine the operational principles of the most important declarative programming paradigms, namely functional and logic programming. Inductively sequential programs admit the definition of optimal computation strategies and are the basis of several rece…
Nick Benton, Andrew Kennedy
A good foreign-language interface is crucial for the success of any modern programming language implementation. Although all serious compilers for functional languages have some facility for interlanguage working, these are often limited and awkward to use.This article describes …
Olaf Chitil
Deforestation optimises a functional program by transforming it into another one that does not create certain intermediate data structures. Short cut deforestation is a deforestation method which is based on a single, local transformation rule. In return, short cut deforestation …
Karl Crary
Many properties of parametric, polymorphic functions can be determined simply by inspection of their types. Such results are usually proven using Reynolds's parametricity theorem. However, Reynolds's theorem can be difficult to show in some settings, particularly ones involving c…
Karl Crary, Stephanie Weirich
Run-time type dispatch enables a variety of advanced optimization techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, and flattened data structures. However, modern type-preserving compilers transform types between stages of co…
Martin Elsman
Berkeley* This paper presents a technique for compiling Standard ML Modules into typed intermediate language fragments, which may be compiled separately and linked using traditional linking technology to form executable code. The technique is called static inteqretataon and allow…
Sigbjørn Finne, Daan Leijen, Erik Meijer, Simon L. Peyton Jones
The increasing popularity of component-based programming tools offer a big opportunity to designers of advanced programming languages, such as Haskell. If we can package our programs as COM objects, then it is easy to integrate them into applications written in other languages. I…
Matthew Flatt, Robert Bruce Findler, Shriram Krishnamurthi, Matthias Felleisen
The MrEd virtual machine serves both as the implementation platform for the DrScheme programming environment, and as the underlying Scheme engine for executing expressions and programs entered into DrScheme's read-eval-print loop. We describe the key elements of the MrEd virtual …
Steven E. Ganz, Daniel P. Friedman, Mitchell Wand
A trampolined program is organized as a single loop in which computations are scheduled and their execution allowed to proceed in discrete steps. Writing programs in trampolined style supports primitives for multithreading without language support for continuations. Various forms…
Neal Glew
Type dispatch constructs are an important feature of many programming languages. Scheme has predicates for testing the runtime type of a value. Java has a class cast expression and a try statement for switching on an exception's class. Crucial to these mechanisms, in typed langua…
Frank Huch
We present an approach for the verification of Erlang programs using abstract interpretation and model checking. In general model checking for temporal logics like LTL and Erlang programs is undecidable. Therefore we define a frame-work for abstract interpretations for a core fra…