2,199 papers · page 81 of 110
We describe and prove the correctness of a new concurrent mark-and-sweep garbage collection algorithm. This algorithm derives from the classical on-the-fly algorithm from Dijkstra et al. [9]. A distinguishing feature of our algorithm is that it supports multiprocessor environment…
The notion that a definition of a variable is dead is used by optimizing compilers to delete code whose execution is useless. We extend the notion of deadness to that of partial deadness, and define a transformation, the revival transformation, which eliminates useless executions…
We show that any monad whose unit and extension operations are expressible as purely functional terms can be embedded in a call-by-value language with “composable continuations”. As part of the development, we extend Meyer and Wand's characterization of the relationship between c…
Formal calculi of record structures have recently been a focus of active research. However, scarcely anyone has studied formally the dual notion—i.e., argument-passing to functions by keywords, and its harmonization with currying. We have. Recently, we introduced the label-select…
The role of non-standard type inference in static program analysis has been much studied recently. Early work emphasised the efficiency of type inference algorithms and paid little attention to the correctness of the inference system. Recently more powerful inference systems have…
The design of a module system for constructing and maintaining large programs is a difficult task that raises a number of theoretical and practical issues. A fundamental issue is the management of the flow of information between program units at compile time via the notion of an …
We unify previous work on the continuation-passing style (CPS) transformations in a generic framework based on Moggi's computational met a-language.This framework is used to obtain GPS transformations for a variety of evaluation strategies and to characterize the corresponding ad…
An important implementation decision in polymorphically typed functional programming language is whether to represent data in boxed or unboxed form and when to transform them from one representation to the other. Using a language with explicit representation types and boxing/unbo…
A theory of combinators in the setting of concurrent processes is formulated. The new combinators are derived from an analysis of the operation called asynchronous name passing, just as an analysis of logical substitution gave rise to the sequential combinators. A system with sev…
RAPIDE is a programming language framework designed for the development of large, concurrent, real-time systems by prototyping. The framework consists of a type language and default executable, specification and architecture languages, along with associated programming tools. We …
International audience
This paper gives a systematic description of several calculi of explicit substitutions. These systems are orthogonal and have easy proofs of termination of their substitution calculus. The last system, called λv, entails a very simple environment machine for strong normalization …
Traditional logic programming languages, such as Prolog, use a fixed left-to-right atom scheduling rule. Recent logic programming languages, however, usually provide more flexible scheduling in which computation generally proceed left-to-right but in which some calls are dynamica…
Automatic parallelization of real FORTRAN programs does not live up to users expectations yet, and dependence analysis algorithms which either produce too many false dependences or are too slow to contribute significantly to this. In this paper we introduce dataflow dependence an…
We develop a calculus in which the computation steps required to execute a computer program can be separated into discrete stages. The calculus, denoted λ2, is embedded within the pure untyped λ-calculus. The main result of the paper is a characterization of sufficient conditions…
Concurrent ML (CML) is an extension of the functional language Standard ML(SML) with primitives for the dynamic creation of processes and channels and for the communication of values over channels. Because of the powerful abstraction mechanisms the communication topology of a giv…
λv is an extension of the λ-calculus with a binding construct for local names. The extension has properties analogous to classical λ-calculus and preserves all observational equivalences of λ. It is useful as a basis for modeling wide-spectrum languages that build on a functional…
An operational semantics for functional logic programs is presented. In such programs functional terms provide for reduction of expressions, provided that they ground. The semantics is based on multi-pass evaluation techniques originally developed for attribute grammars. Program …
This paper describes a method for detecting structural hazards 5--80 times faster than its predecessors, which generally have simulated the pipeline at compile time. It accepts a compact specification of the pipeline and creates a finitestate automaton that can detect structural …
Higher-order equational logic programming is a paradigm which combines first-order equational and higher-order logic programming, where higher-order logic programming is based on a subclass of simply typed l-terms, called higher-order patterns. Central to the notion of higher-ord…