title: Static and Dynamic Semantics Processing

authors:
Charles Consel
Olivier Danvy

abstract: This paper presents a step forward in the use of partial evaluation for interpreting and compiling programs, as well as for automatically generating a compiler from denotational definitions of programming languages. We determine the static and dynamic semantics of a programming language, reduce the expressions representing the static semantics, and generate object code by instantiating the expressions representing the dynamic semantics. By processing the static semantics of the language, programs get compiled. By processing the static semantics of the partial evaluator, compilers are generated. The correctness of a compiler is guaranteed by the correctness of both the executable specification and our partial evaluator. The results reported in this paper improve on previous work in the domain of compiler generation [16, 30], and solves several open problems in the domain of partial evaluation [15]. In essence: ffl Our compilation goes beyond a mere syntax-tosemantics mapping since the ...


venue: popl

title: Parameter-Passing and the Lambda Calculus

authors:
Erik Crank
Matthias Felleisen

abstract: The choice of a parameter-passing technique is an important decision in the design of a high-level programming language. To clarify some of the semantic aspects of the decision, we develop, analyze, and compare modifications of the $\\lambda$-calculus for the most common parameter-passing techniques. More specifically, for each parameter-passing technique we provide (1) a program rewriting semantics for a language with side-effects and first-class procedures based on the respective parameter-passing technique; (2) an equational theory derived from the rewriting semantics; (3) a formal analysis of the correspondence between the calculus and the semantics; and (4) a strong normalization theorem for the largest possible imperative fragment of the theory.\nA comparison of the various systems reveals that Algol's call-by-name indeed satisfies the well-known $\\beta$ rule of the original $\\lambda$-calculus, but at the cost of complicated axioms for the imperative part of the theory. The simplest and most appealing axiom system appears to be the one for a call-by-value language with reference cells as first-class values.


title: Typing First-Class Continuations in ML

authors:
Bruce F. Duba
Robert Harper
David B. MacQueen

abstract: An extension of Standard ML with continuation primitives similar to those found in Scheme is considered.A number of alternative type systems are discussed, and several programming examples are given.The semantics of type assignment for a small, purely functional fragment of the language is presented, for which both a Milner-style soundness theorem and an observational soundness theorem may be established.


title: A Record Calculus Based on Symmetric Concatenation

authors:
Robert Harper
Benjamin C. Pierce

abstract: Type systems for operations on extensible records form sumpt ion; we argue that the resulting system is more straightforward than subsumption-based alternatives.


title: The Complexity of Type Inference for Higher-Order Typed Lambda Calculi

authors:
Fritz Henglein
Harry G. Mairson

abstract: We analyze the computational complexity of type inference for untyped A.terms in the second-order polymorphic typed ~-calculus (l'z) invented by Gi-


title: Temporal Proof Methodologies for Real-time Systems

authors:
Thomas A. Henzinger
Zohar Manna
Amir Pnueli

abstract: . We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of concurrent and reactive systems. A global, discrete, and asynchronous clock is incorporated into the model by defining the abstract notion of a real-time transition system as a conservative extension of traditional transition systems: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upperbound real-time requirements for transitions. We show how to model real-time systems that communicate either through shared variables or by message passing, and how to represent the important real-time constructs of priorities (interrupts), scheduling, and timeouts in this framework. Two styles for the specification of real-time properties are presented. The first style uses bounded versions of the temporal operators; the real-time requirements expressed in this style are classified ...


title: Coordinating First-Order Multiparty Interactions

authors:
Yuh-Jzer Joung
Scott A. Smolka

abstract: A first-order multiparty interaction is an abstraction mechanism that defines communication among a set of formal process roles. Actual processes participate in a first-order interaction by enroling into roles, and execution of the interaction can proceed when all roles are filled by distinct processes. As in CSP, enrolement statements can serve as guards in alternative commands. The enrolement guard scheduling problem then is to enable the execution of first-order interactions through the judicious scheduling of roles to processes currently ready to execute enrolement guards. We present a fully distributed and message-efficient algorithm for the enrolement guard scheduling problem, the first such solution of which we are aware. We also describe several extensions of the algorithm, including generic roles, dynamically changing environments where processes can be created and destroyed at run time, and nested-enrolement which allows interactions to be nested.


title: Algebraic Reconstruction of Types and Effects

authors:
Pierre Jouvelot
David K. Gifford

abstract: We present the first algorithm for reconstructing the types and effects of expressions in the presence of first class procedures in a polymorphic typed language, Effects are static descriptions of the dynamic behavior of expressions.Just as a type describes what an expression computes, an effect describes howan expression computes.Types are more complicated to reconstruct in the presence of effects because the algebra of effects induces complex constraints on both effects and types.In this paper we show how to perform reconstruction in the presence of such constraints with a new algorithm called algebraic reconstruction, prove that it is sound and complete, and discuss its practical import.


title: Communication with Directed Logic Variables

authors:
Alon Kleinman
Yael Moscowitz
Amir Pnueli
Ehud Shapiro


title: Pointer-Induced Aliasing: A Problem Classification

authors:
William Landi
Barbara G. Ryder

abstract: A?iasing occurs at some program point during execution when two or more names exist for the same location. We have isolated various programming language mechanisms which create aliases. We have classified the complexity of the fllas problem induced by each mechanism alone and in combination, as AfP-hard, complement tip-hard, or polynomial (’P). We present our problem classification, give an overview of our proof that finding interprocedural aliases in the presence of single level pointers is in 7, and present a represent tive proof for the NP-hard problems.


title: Polymorphic Type Inference and Assignment

authors:
Xavier Leroy
Pierre Weis

abstract: We present a new approach to the polymorphic typing of data accepting in-place modification in ML-like languages.This approach is based on restrictions over type generalization, and a refined typing of functions.The type system given here leads to a better integration of imperative programming style with the purely applicative kernel of ML.In particular, generic functions that allocate mutable data can safely be given fully polymorphic types.We show the soundness of this type system, and give a type reconstruction algorithm.


title: Parallel Programming With Coordination Structures

authors:
Steven Lucco
Oliver Sharp

abstract: Parallel programs display two fundamentally different kinds of execution behavior: synchronous and asynchronous.Some methodologies, such as distributed data structures, are best suited to the construction of asynchronous programs.In this paper, we propose a methodology for synchronous parallel programming based on the notion of a coordination structure, a direct representation of the multidimensional dataflow patterns common to synchronous programs.We introduce Delirium, a language in which one can concisely express many useful coordination structures.


title: Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems

abstract: We introduce the new framework of Labeled


title: An Extension of Standard ML Modules with Subtyping and Inheritance

authors:
John C. Mitchell
Sigurd Meldal
Neel Madhav

abstract: We describe a general module language integrating abstract data types, specifications and object-oriented concepts. The framework is based on the Standard ML module system, with three main extensions: subtyping, a form of object derived from ML structures, and inheritance primitives. The language aims at supporting a range of programming styles, including mixtures of object-oriented programming and programs built around specified algebraic or higher-order abstract data types. We separate specification from implementation, and provide independent inheritance mechanisms for each. In order to support binary operations on objects within this framework, we introduce "internal interfaces" which govern the way that function components of one structure may access components of another. The language design has been tested by writing a number of program examples; an implementation is under development in the context of a larger project. 1 Introduction This paper describes a general module sys...


title: How to Make Destructive Updates Less Destructive

abstract: We present a safe embedding of mutable data structures in functional languages. With safety we mean that confluence and (in some sense) referential transparency are maintained. We develop a static criterion based on abstract interpretation which checks that any side-effect which a function may exert via a destructive update remains invisible. The technique opens up the possibility of designing safe and efficient wide-spectrum languages which combine functional and imperative language constructs.


title: Dependence Flow Graphs: An Algebraic Approach to Program Dependencies

authors:
Keshav Pingali
Micah D. Beck
Richard Johnson
Mayan Moudgill
Paul Stodghill

abstract: The topic of intermediate languages for optimizing and parallelizing compilers has received muchattention lately. In this paper, we argue that any good representation of a program must havetwo crucial properties: first, it must be a data structure that can be rapidly traversed to determine dependence information, and second this representation must be a program in its own right, with a parallel, local model of execution. In this paper, we illustrate the importance of these points by examining algorithms for a standard optimization --- global constant propagation. We discuss the problems in working with current representations. Then, we propose a novel representation called the dependence flow graph which has each of the properties mentioned above. Weshow that this representation leads to a simple algorithm, based on abstract interpretation, for solving the constant propagation problem. Our algorithm is simpler than, and as efficient as, the best known algorithms for this problem. An interesting feature of our representation is that it naturally incorporates the best aspects of many other representations, including continuation-passing style, data and program dependence graphs, static single assignment form and dataflow program graphs.


title: Program Optimization and Parallelization Using Idioms

authors:
Shlomit S. Pinter
Ron Y. Pinter

abstract: Programs in languages such as FORTRAN, Pascal, and which our method indeed outperforms existing analysis techniques.


title: Modeling Concurrency with Geometry

abstract: The phenomena of branching time and true or noninterleaving concurrency find their respective homes in automata and schedules.But these two models of computation are formally equivalent via Birkhoff duality, an equivalence we expound on here in tutorial detail.So why should these phenomena prefer one over the other?We identify dimension as the culprit: l-dimensional automata are skeletons permitting only interleaving concurrency, whereas true n-fold concurrency resides in transitions of dimension n.The truly concurrent automaton dual to a schedule is not a skeletal distributive lattice but a solid one!We introduce true nondeterminism and define it as monoidal homotopy; from this perspective nondeterminism in ordinary automata arises from forking and joining creating nontrivial homotopy, The automaton dual to a poset schedule is simply connected whereas that dual to an event structure schedule need not be, according to monoidal homotopy though not to group homotopy.We conclude with a formal definition of higher dimensional automaton as an n-complex or n-category, whose two essential axioms are associativity of concatenation within dimension and an interchange principle between dimensions. 1 Background A central problem in the semantics of imperative computation is the construction of convenient models of computation embodying the apparent aspects of both branching time and true or noninterleaving or causal t


title: A Dynamic Extent Control Operator for Partial Continuations

authors:
Christian Queinnec
Bernard P. Serpette

abstract: A partial continuation is a prefix of the computation that remains to be done.We propose in this paper a new operator which precisely controls which prefix is to be abstracted into a partial continuation.This operator is strongly related to the notion of dynamic extent which we denotationally characterize.Some programming examples are commented and we also show how to express previously proposed control operators.A suggested implementation is eventually discussed.


title: Fully Abstract Translations between Functional Languages

abstract: Article Fully abstract translations between functional languages Share on Author: Jon G. Riecke MIT Laboratory for Computer Science MIT Laboratory for Computer ScienceView Profile Authors Info & Claims POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1991 Pages 245–254https://doi.org/10.1145/99583.99617Online:03 January 1991Publication History 21citation355DownloadsMetricsTotal Citations21Total Downloads355Last 12 Months11Last 6 weeks4 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access


title: Semantic Foundations of Concurrent Constraint Programming

authors:
Vijay A. Saraswat
Martin C. Rinard
Prakash Panangaden

abstract: Concurrent constraint programming [Sar89 ,SR90] is a simple and powerful model of concurrent computation based on the notions of store-as-constraint and process as information combinators in the language, can be used for proving liveness properties of programs, and is fully abstract with respect to the obvious notion of observation.


title: On the Power and Limitation of Strictness Analysis Based on Abstract Interpretation

authors:
R. C. Sekar
Prateek Mishra
I. V. Ramakrishnan

abstract: Strictness analysis based on abstract interpretation is an important technique for optimization of lazy functional languages.It is well known that all strictness analysis methods are incomplete, i.e., fail to report some strictness properties.In this paper, we provide the first precise and formal characterization of the loss of information that leads to this incompleteness.Specifically, we establish the following characterization theorem for Mycroft's method called old-analysis.


title: Modeling Continuations without Continuations

authors:
Dorai Sitaram
Matthias Felleisen

abstract: Article Free Access Share on Models of continuations without continuations Authors: Dorai Sitaram Department of Computer Science, Rice University, Houston, TX Department of Computer Science, Rice University, Houston, TXView Profile , Matthias Felleisen Department of Computer Science, Rice University, Houston, TX Department of Computer Science, Rice University, Houston, TXView Profile Authors Info & Claims POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1991 Pages 185–196https://doi.org/10.1145/99583.99611Online:03 January 1991Publication History 4citation439DownloadsMetricsTotal Citations4Total Downloads439Last 12 Months7Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Incremental Compilation via Partial Evaluation

authors:
R. S. Sundaresh
Paul Hudak

abstract: Article A theory of incremental computation and its application Share on Authors: R. S. Sundaresh Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CT Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CTView Profile , Paul Hudak Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CT Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CTView Profile Authors Info & Claims POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesJanuary 1991 Pages 1–13https://doi.org/10.1145/99583.99587Online:03 January 1991Publication History 22citation447DownloadsMetricsTotal Citations22Total Downloads447Last 12 Months7Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access


title: Optimally Profiling and Tracing Programs

authors:
Thomas Ball
James R. Larus

abstract: This paper describes algorithms for inserting monitoring code to profile and trace programs. These algorithms greatly reduce the cost of measuring programs with respect to the commonly used technique of placing code in each basic block. Program profiling counts the number of times each basic block in a program executes. Instruction tracing records the sequence of basic blocks traversed in a program execution. The algorithms optimize the placement of counting/tracing code with respect to the expected or measured frequency of each block or edge in a program's control-flow graph. We have implemented the algorithms in a profiling/tracing tool, and they substantially reduce the overhead of profiling and tracing.We also define and study the hierarchy of profiling problems. These problems have two dimensions: what is profiled (i.e., vertices (basic blocks) or edges in a control-flow graph) and where the instrumentation code is placed (in blocks or along edges). We compare the optimal solutions to the profiling problems and describe a new profiling problem: basic-block profiling with edge counters. This problem is important because an optimal solution to any other profiling problem (for a given control-flow graph) is never better than an optimal solution to this problem. Unfortunately, finding an optimal placement of edge counters for vertex profiling appears to be a hard problem in general. However, our work shows that edge profiling with edge counters works well in practice because it is simple and efficient and finds optimal counter placements in most cases. Furthermore, it yields more information than a vertex profile. Tracing also benefits from placing instrumentation code along edges rather than on vertices.


title: Modeling Prolog Control

authors:
Roberto Barbuti
Michael Codish
Roberto Giacobazzi
Giorgio Levi


title: Recognizing Substrings of LR(k) Languages in Linear Time

authors:
Joseph Bates
Alon Lavie

abstract: LR parsing techniques have long been studied as efficient and powerful methods for processing context free languages. A linear time algorithm for recognizing languages representable by LR(k) grammars has long been known. Recognizing substrings of a context-free language is at least as hard as recognizing full strings of the language, as the latter problem easily reduces to the former. In this paper we present a linear time algorithm for recognizing substrings of LR(k) languages, thus showing that the substring recognition problem for these languages is no harder than the full string recognition problem. An interesting data structure, the Forest Structured Stack, allows the algorithm to track all possible parses of a substring without loosing the efficiency of the original LR parser. We present the algorithm, prove its correctness, analyze its complexity, and mention several applications that have been constructed.


title: A Semantics for ML Concurrency Primitives

authors:
Dave Berry
Robin Milner
David N. Turner

abstract: We present a set of concurrency primitives for Standard ML. We define these by giving the transitional semantics of a simple language. We prove that our semantics preserves the expected behaviour of sequential programs. We also show that we can define stores as processes, such that the representation has the same behaviour as a direct definition. These proofs are the first steps towards integrating our semantics with the full definition of Standard ML.


title: PER Models of Subtyping, Recursive Types and Higher-Order Polymorphism

authors:
Kim B. Bruce
John C. Mitchell


title: Observable Sequentiality and Full Abstraction

authors:
Robert Cartwright
Matthias Felleisen

abstract: ion Robert Cartwright Matthias Felleisen Department of Computer Science Rice University Houston, TX 77251-1892 Rice Technical Report CS 91-167 A preliminary version of this technical report appeared in the Proceedings of the 19th Annual ACM Symposium on Principles of Programming Languages, January 19--22, 1992, Albuquerque, New Mexico. Copyright c fl1992 by Robert Cartwright and Matthias Felleisen 1 Full Abstraction and Sequentiality 1 1.1 Summary of Previous Work : : : : : : : : : : : : : : : : : : : : : : : : : : : 2 1.2 Summary of Results : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 2 PCF 4 2.1 Formal Semantics : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5 2.2 Observational Equivalence, Sequentiality : : : : : : : : : : : : : : : : : : : : 8 3 Observing Sequentiality 9 3.1 Using errors, programmers can observe the order of evaluation. : : : : : : : 10 3.2 Using control operators, programs can observe the order of evaluation. : : : 10...


title: Compile-Time Analysis of Parallel Programs that Share Memory

authors:
Jyh-Herng Chow
Williams Ludwell Harrison III

abstract: Traditional optimization techniques for sequential programs are not directly applicable to parallel programs where concurrent activities may interfere with each other through shared variables. New compiler techniques must be developed to accommodate features found in parallel languages. In this paper, we use abstract interpretation to obtain useful properties of programs, e.g., side effects, data dependences, object lifetime and concurrent expressions, for a language that supports first-class functions, pointers, dynamic allocations and explicit parallelism through cobegin. These analyses may facilitate many applications, such as program optimization, parallelization, restructuring, memory management, and detecting access anomalies.


title: Model Checking and Abstraction

authors:
Edmund M. Clarke
Orna Grumberg
David E. Long

abstract: We describe a method for using abstraction to reduce the complexity of temporal logic model checking. The basis of this method is a way of constructing an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a pipelined ALU circuit with over 101300 states.


title: Type Isomorphisms in a Type-Assignment Framework

abstract: This paper contains a full treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. Surprisingly enough the results obtained contradict the common-place feeling that (the core of) ML is a subset of second order λ-calculus: we can provide an isomorphism of types that holds in the core ML language, but not in second order λ-calculus. This new isomorphism not only allows to provide a complete (and decidable) axiomatisation of all the type isomorphic in ML style languages, a relevant issue for the type as specifications paradigm in library searches, but also suggest a natural extension that in a sense completes the type-inference mechanism in ML. This extension is easy to implement and allows to get a further insight in the nature of the let polymorphic construct.


title: Inductive Definitions, Semantics and Abstract Interpretation

authors:
Patrick Cousot
Radhia Cousot

abstract: We introduce and illustrate a specification method combining rule-based inductive definitions, well-founded induction principles, fixed-point theory and abstract interpretation for general use in computer science. Finite as well as infinite objects can be specified, at various levels of details related by abstraction. General proof principles are applicable to prove properties of the specified objects.


title: A Mark-and-Sweep Collector for C++

abstract: Our research is concerned with compiler-independent, tag-free garbage collection for the C++ programming language. We have previously presented a copying collector based on root registration. This paper presents a mark-and-sweep garbage collector that ameliorates shortcomings of the previous collector. We describe the two collectors and discuss why the new one is an improvement over the old one. We have tested this collector and a conservative collector in a VLSI CAD application, and this paper discusses the differences. Currently this prototype of the collector imposes too much overhead on our application. We intend to solve that problem, and then use the techniques described in this paper to implement a generational Mark-and-Sweep collector for C++.


title: Pattern-Based Tree Attribution

abstract: Attribute grammars have been used for many language-oriented tasks, including the formal description of semantics and the implementation of compilation tasks from simple type checking through code generation. Despite their successful use, attribute grammars have some disadvantages, including the monolithic nature of the grammar and the fixed factoring of all attribute descriptions by a single set of grammar productions. Attribute pattern sets provide a more expressive attribution system by using pattern matching, instead of grammar productions, to perform case analysis. Attribute pattern sets can be implemented in terms of attribute grammars in a way that maintains the dependency structure of the attribute system, making it straightforward to convert many of the practical results from attribute grammar theory to similar results for attribute pattern sets.


title: Composable Attribute Grammars: Support for Modularity in Translator Design and Implementation

authors:
Rodney Farrow
Thomas J. Marlowe
Daniel M. Yellin

abstract: This paper introduces Composable Attribute Grammars (CAGs), a formalism that extends classical attribute grammars to allow for the modular composition of translation specifications and of translators. CAGs bring to complex translator writing systems the same benefits of modularity found in modern programming languages, including comprehensibility, reusability, and incremental meta-compilation.A CAG is built from several smaller component AGs, each of which solves a particular subproblem, such as name analysis or register allocation. A component AG is based upon a simplified phrase-structure that reflects the properties of its subproblem rather than the phrase-structure of the source language. Different component phrase-structures for various subproblems are combined by mapping them into a phrase-structure for the source language. Both input and output attributes can be associated with the terminal symbols of a component AG. Output attributes enable the results of solving a subproblem to be distributed back to anywhere that originally contributed part of the subproblem, e.g. transparently distributing the results of global name analysis back to every symbolic reference in the source program.After introducing CAGs by way of an example, we provide a formal definition of CAGs and their semantics. We describe a subclass of CAGs and their semantics. We describe a subclass of CAGs, called separable CAGs, that have favorable implementation properties. We discuss the novel aspects of CAGs, compare them to other proposals for inserting modularity into attribute grammars, and relate our experience using CAGs in the Linguist translator-writing system.


title: Linear Continuations

abstract: We present a functional interpretation of classical linear logic based on the concept of linear continuations. Unlike their non-linear counterparts, such continuations lead to a model of control that does not inherently impose any particular evaluation strategy. Instead, such additional structure is expressed by admitting closely controlled copying and discarding of continuations. We also emphasize the importance of classicality in obtaining computationally appealing categorical models of linear logic and propose a simple “coreflective subcategory” interpretation of the modality “!”.


title: The Geometry of Optimal Lambda Reduction

authors:
Georges Gonthier
Martín Abadi
Jean-Jacques Lévy

abstract: Lamping discovered an optimal graph-reduction implementation of the λ-calculus. Simultaneously, Girard invented the geometry of interaction, a mathematical foundation for operational semantics. In this paper, we connect and explain the geometry of interaction and Lamping's graphs. The geometry of interaction provides a suitable semantic basis for explaining and improving Lamping's system. On the other hand, graphs similar to Lamping's provide a concrete representation of the geometry of interaction. Together, they offer a new understanding of computation, as well as ideas for efficient and correct implementations.


title: Generalized Dominators and Post-Dominators

abstract: The notion of dominators is generalized to include multiple-vertex dominators in addition to single-vertex dominators. A multiple-vertex dominator of a vertex is a group of vertices that collectively dominate the vertex. Existing algorithms compute immediate single-vertex dominators, and an algorithm for computing immediate multiple-vertex dominators is presented in this paper. The immediate dominator information is expressed in the form of a directed acyclic graph referred to as the dominator DAG or the DDAG. The generalized dominator set of any vertex dominators of the vertex, can be computed from the DDAG. The single-vertex dominator information restricts the propagation of loop invariant statements and array bound checks out of loops. Generalized dominator information avoids these restrictions. In addition, it can be used to identify natural loops and improve the existing optimization algorithm for code hoisting. The dual notion of generalized post-dominators can be used for computing control dependences and automatic generation of compact test suites for programs.


title: Abstract Semantics for a Higher-Order Functional Language with Logic Variables

authors:
Radha Jagadeesan
Keshav Pingali

abstract: Althoughthere is considerable experience in using languages that combine the functional and logic program-


title: Generating a Compiler for a Lazy Language by Partial Evaluation

abstract: Compiler generation is often emphasized as being the most important application of partial evaluation. But most of the larger practical applications have, to the best of our knowledge, been outside this field. Expecially, no one has generated compilers for languages other than small languages. This paper describes a large application of partial evaluation where a realistic compiler was generated for a strongly typed lazy functional language. The language, that was called BAWL, was modeled after the language in Bird and Wadler [BW88] and is a combinator language with pattern matching, guarded alternatives, local definitions and list comprehensions. The paper describes the most important techniques used, especially the binding time improvements needed in order to get small and efficient target programs. Finally, the performance of the compiler is compared with two compilers for similar languages: Miranda and LML.


title: A Comprehensive Study of the Complexity of Multiparty Interaction

authors:
Yuh-Jzer Joung
Scott A. Smolka

abstract: We present a taxonomy of languages for multiparty interaction, which covers all proposals of which we are aware. Based on this taxonomy, we present a comprehensive analysis of the computational complexity of the multiparty interaction implementation problem, the problem of scheduling multiparty interactions in a given execution environment.


title: Garbage Collecting the World

authors:
Bernard Lang
Christian Queinnec
José M. Piquer

abstract: Distributed symbolic computations involve the existence of remote references allowing an object, local to a processor, to designate another object located on another processor. To reclaim inaccessible objects is the non trivial task of a distributed Garbage Collector (GC). We present in this paper a new distributed GC algorithm which (i) is fault-tolerant, (ii) is largely independent of how a processor garbage collects its own data space, (iii) does not need centralized control nor global stop-the-world synchronization, (iv) allows for multiple concurrent active GCs, (v) does not require to migrate objects from processor to processor and (vi) eventually reclaims all inaccessible objects including distributed cycles.


title: Unboxed Objects and Polymorphic Typing

abstract: This paper presents a program transformation that allows languages with polymorphic typing (e.g. ML) to be implemented with unboxed, multi-word data representations. The transformation introduces coercions between various representations, based on a typing derivation. A prototype ML compiler utilizing this transformation demonstrates important speedups.


title: Algorithmic Aspects of Type Inference with Subtypes

authors:
Patrick Lincoln
John C. Mitchell

abstract: We study the complexity of type inference for programming languages with subtypes. There are three language variations that effect the problem: (i) basic functions may have polymorphic or more limited types, (ii) the subtype hierarchy may be fixed or vary as a result of subtype declarations within a program, and (iii) the subtype hierarchy may be an arbitrary partial order or may have a more restricted form, such as a tree or lattice. The naive algorithm for infering a most general polymorphic type, undervariable subtype hypotheses, requires deterministic exponential time. If we fix the subtype ordering, this upper bound grows to nondeterministic exponential time. We show that it is NP-hard to decide whether a lambda term has a type with respect to a fixed subtype hierarchy (involving only atomic type names). This lower bound applies to monomorphic or polymorphic languages. We give PSPACE upper bounds for deciding polymorphic typability if the subtype hierarchy has a lattice structure or the subtype hierarchy varies arbitrarily. We also give a polynomial time algorithm for the limited case where there are of no function constants and the type hierarchy is either variable or any fixed lattice.


title: Parametricity as Subtyping

abstract: A polymorphic function is parametric if it has uniform behavior for all type parameters. This property is useful when writing, reasoning about, and compiling functional programs.


title: Bounded Fixed Point Iteration

authors:
Hanne Riis Nielson
Flemming Nielson

abstract: In the context of abstract interpretation we study the number of times a functional need to be unfolded in order to give the least fixed point. For the cases of the total or monotone functions we obtain an exponential bound and in the case of strict and additive (or distributive) functions we obtain a quadratic bound. These bounds are shown to be tight. Specialising the case of strict and additive functions to functionals of a form that would correspond to iterative programs we show that a linear bound is tight. We demonstrate the relation to several analyses studied in the literature (including strictness analysis).


title: Partial Evaluation of High-Level Imperative Programming Languages, with Applications in Hard Real-Time Systems

authors:
Vivek Nirkhe
William W. Pugh

abstract: Article Free Access Share on Partial evaluation of high-level imperative programming languages with applications in hard real-time systems Authors: Vivek Nirkhe View Profile , William Pugh View Profile Authors Info & Claims POPL '92: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesFebruary 1992 Pages 269–280https://doi.org/10.1145/143165.143223Published:01 February 1992Publication History 25citation374DownloadsMetricsTotal Citations25Total Downloads374Last 12 Months15Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: A Compilation Method for ML-Style Polymorphic Record Calculi

abstract: Polymorphic record calculi have recently attracted much attention as a typed foundation for object-oriented programming. This is based on the fact that a function that selects a field l of a record can be given a polymorphic type that enables it to be applied to various records containing a field l. Recent studies have established techniques to develop an ML-style type inference algorithm for such a polymorphic type system. There seems to be, however, no established method to compile an ML-style polymorphic record calculus into efficient code. The purpose of this paper is to present one such method. We define a polymorphic record calculus as an extension of Damas and Miler's proof system for ML. For this calculus, we define an implementation calculus where records are represented as arrays of (references to) values and field selection is performed by direct indexing. To represent polymorphic field selection, the implementation calculus contains an abstraction mechanism over indexes. We then develop an algorithm to translate the polymorphic record calculus into the implementation calculus by refining a type inference algorithm; it simultaneously computes a principal type scheme in the polymorphic record calculus and a correct implementation term in the implementation calculus. The type inference is shown to be sound and complete in the sense of Damas-Milner's algorithm for ML. Moreover, the polymorphic type system is shown to be sound with respect to an operational semantics of the translated terms in the implementation calculus.


title: Bounded Quantification is Undecidable

abstract: F≤ is a typed λ-calculus with subtyping and bounded second-order polymorphism. First proposed by Cardelli and Wegner, it has been widely studied as a core calculus for type systems with subtyping.


title: Typing Record Concatenation for Free

abstract: We show that any functional language with record extension possesses record concatenation for free. We exhibit a translation from the latter into the former. We obtain a type system for a language with record concatenation by composing the translation with type-checking in a language with record extension. We apply this method to a version of ML with a record extension and obtain an extension of ML with either asymmetric or symmetric concatenation. The latter extension is simple, flexible and has a very efficient type inference algorithm in practice. Concatenation together with removal of fields needs one more construct than extension of records. It can be added to the version of ML with record extension. However, many typed languages with record cannot type such a construct. The method still applies to them, producing type systems for record concatenation without removal of fields. Object systems also benefit of the encoding which shows that multiple inheritance does not actually require the concatenation of records but only their extension.


title: Semantic Foundations of Jade

authors:
Martin C. Rinard
Monica S. Lam

abstract: Jade is a language designed to support coarse-grain parallelism on both shared and distributed address-space machines. Jade is data-oriented: a Jade programmer simply augments a sequential imperative program with declarations specifying how the program accesses data. A Jade implementation dynamically interprets the access specification to execute the program concurrently while enforcing the program's data dependence constraints, thus preserving the sequential semantics.


title: Principal Signatures for Higher-Order Program Modules

abstract: Under the Damas-Milner type discipline for functional languages, every expression has principal type, if it elaborates at all. In the type discipline for ML Modules, a signature expression has a principal signature, if it elaborates at all. However, while functions can be higher-order in ML, parameterised modules in ML are first-order only. We present a type discipline for a skeletal higher-order module language which has principal signatures. Sharing and multiple views of structures are handled in a manner which is compatible with the semantics of the first-order ML modules.


title: The Essence of Functional Programming

abstract: This paper explores the use monads to structure functional programs. No prior knowledge of monads or category theory is required.


title: Formal Parametric Polymorphism

authors:
Martín Abadi
Luca Cardelli
Pierre-Louis Curien

abstract: A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds' work, the study of parametricity is typically semantic. In this paper, we develop a syntactic approach to parametricity, and a formal system that embodies this approach: system ℜ. Girard's system F deals with terms and types; ℜ is an extension of F that deals also with relations between types.


title: Evicted Variables and the Interaction of Global Register Allocation and Symbolic Debugging

authors:
Ali-Reza Adl-Tabatabai
Thomas R. Gross

abstract: A symbolic debugger allows a user to display the values of program variables at a breakpoint. However, problems arise if the program is translated by an optimizing compiler. This paper addresses the effects of global register allocation and assignment: a register assigned to a variable V may not be holding V's value at a breakpoint since the register can also be assigned to other variables. We define the problem of determining whether a variable is in its assigned register as the residence problem. Prior work on debugging of optimized code has focused on the currency problem; detecting whether a variable's run-time value is the expected value. Determining residence is a more serious problem than currency detection. We present a data flow algorithm that accurately computes a variable's residency, by determining when a variable becomes evicted from its register. We measure the effectiveness of different approaches to determine variable residence for three C programs from the SPEC suite.


title: Extending Record Typing to Type Parametric Modules with Sharing

abstract: We extend term unification techniques used to type extensible records in order to solve the two main typing problems for modules in Standard ML: matching and sharing. We obtain a type system for modules based only on well known unification problems, modulo some equational theories we define. Our formalization is simple and has the elegance of polymorphic type disciplines based on unification. It can be seen as a synthesis of previous work on module and record typing.


title: Incremental Program Testing Using Program Dependence Graphs

authors:
Samual Bates
Susan Horwitz

abstract: Program dependence graphs have been proposed for use in optimizing, vectorizing, and parallelizing compilers, and for program integration. This paper proposes their use as the basis for incremental program testing when using test data adequacy criteria. Test data adequacy is commonly used to provide some confidence that a particular test suite does a reasonable job of testing a program. Incremental program testing using test data adequacy criteria addresses the problem of testing a modified program given an adequate test suite for the original program. Ideally, one would like to create an adequate test suite for the modified program that reuses as many files from the old test suite as possible. Furthermore, one would like to know, for every file that is in both the old and the new test suites, whether the program components exercised by that file have been affected by the program modification; if no components have been affected, then it is not necessary to rerun the program using that file.In this paper we define adequacy criteria based on the program dependence graph, and propose techniques based on program slicing to identify components of the modified program that can be tested using files from the old test suite, and components that have been affected by the modification. This information can be used to reduce the time required to create new test files, and to avoid unproductive retesting of unaffected components. Although exact identification of the components listed above is, in general, undecidable, we demonstrate that our techniques provide safe approximations.


title: Communicating Reactive Processes

authors:
Gérard Berry
S. Ramesh
R. K. Shyamasundar

abstract: We present a new programming paradigm called Communicating Reactive Processes or CRP that unifies the capabilities of asynchronous and synchronous concurrent programming languages. Asynchronous languages such as CSP, Occam, or Ada are well-suited for distributed algorithms; their processes are loosely coupled and communication takes time. The Esterel synchronous language is dedicated to reactive systems; its processes are tightly coupled and deterministic, communication being realized by instantaneous broadcasting. Complex applications such as process or robot control require to couple both forms of concurrency, which is the object of CRP. A CRP program consists of independent locally reactive Esterel nodes that communicate with each other by CSP rendezvous. CRP faithfully extends both Esterel and CSP and adds new possibilities such as precise local watchdogs on rendezvous. We present the design of CRP, its semantics, a translation into classical process calculi for program verificatio...


title: Differential Logic Programming

authors:
Annalisa Bossi
Michele Bugliesi
Maurizio Gabbrielli
Giorgio Levi
Maria Chiara Meo

abstract: In this paper we define a compositional semantics for a generalized composition operator on logic programs. Static and dynamic inheritance as well as composition by union of clauses can all be obtained by specializing the general operator. The semantics is based on the notion of differential programs, logic programs annotated with declarations that establish the programs' external interfaces.


title: Safe Type Checking in a Statically-Typed Object-Oriented Programming Language

abstract: In this paper we introduce a statically-typed, functional, object-oriented programming language, TOOPL, which supports classes, objects, methods, instance variable, subtypes, and inheritance.


title: Automatic Array Alignment in Data-Parallel Programs

authors:
Siddhartha Chatterjee
John R. Gilbert
Robert Schreiber
Shang-Hua Teng

abstract: Data-parallel languages like Fortran 90 express parallelism in the form of operations on data aggregates such as arrays. Misalignment of the operands of an array operation can reduce program performance on a distributed-memory parallel machine by requiring nonlocal data accesses. Determining array alignments that reduce communication is therefore a key issue in compiling such languages.


title: Efficient Flow-Sensitive Interprocedural Computation of Pointer-Induced Aliases and Side Effects

authors:
Jong-Deok Choi
Michael G. Burke
Paul R. Carini

abstract: We present practical approximation methods for computing interprocedural aliases and side effects for a program written in a language that includes pointers, reference parameters and recursion. We present the following results: 1) An algorithm for flow-sensitive interprocedural alias analysis which is more precise and efficient than the best interprocedural method known. 2) An extension of traditional flow-insensitive alias analysis which accommodates pointers and provides a framework for a family of algorithms which trade off precision for efficiency. 3) An algorithm which correctly computes side effects in the presence of pointers. Pointers cannot be correctly handled by conventional methods for side effect analysis. 4) An alias naming technique which handles dynamically allocated objects and guarantees the correctness of data-flow analysis. 5) A compact representation based on transitive reduction which does not result in a loss of precision and improves precision in some case. 6) A method for intraprocedural alias analysis which is based on a sparse representation.


title: Layer Sharing: An Improved Structure-Sharing Framework

abstract: We present in this paper a structure–sharing framework originally developed for a Dynamic Programming interpreter of Logic programs called DyALog. This mechanism should be of interest for alternative execution models of PROLOG which maintain multiple computation branches and reuse sub-computations in various contexts (computation sharing). This category includes, besides our Dynamic Programming model, the tabular models (OLDT, SLDAL, XWAM), the “magic-set” models, and the independent AND and OR parallelism with solution sharing models. These models raise the problem of storing vast amount of data, motivating us to discard copying mechanisms in favor of structure-sharing mechanisms. Unfortunately, computation sharing requires joining computation branches and possibly renaming some variables, which generally leads to complex structure-sharing mechanisms. The proposed “layer-sharing” framework succeeds however in remaining understandable and easy to implement.


title: Compositional Analysis of Modular Logic Programs

authors:
Michael Codish
Saumya K. Debray
Roberto Giacobazzi

abstract: This paper describes a semantic basis for a compositional approach to the analysis of logic programs. A logic program is viewed as consisting of a set of modules, each module defining a subset of the program's predicates. Analyses are constructed by considering abstract interpretations of a compositional semantics. The abstract meaning of a module corresponds to its analysis and composition of abstract meanings corresponds to composition of analyses. Such an approach is essential for large program development so that altering one module does not require re-analysis of the entire program. We claim that for a substantial class of programs, compositional analyses which are based on a notion of abstract unfolding provide the same precision as non-compositional analysis. A compositional analysis for ground dependencies is included to illustrate the approach. To the best of our knowledge this is the first account of a compositional framework for the analysis of logic programs.


title: Tutorial Notes on Partial Evaluation

authors:
Charles Consel
Olivier Danvy

abstract: The last years have witnessed a flurry of new results in the area of partial evaluation. These tutorial notes survey the field and present a critical assessment of the state of the art.


title: Complexity of Bidirectional Data Flow Analysis

authors:
Dhananjay M. Dhamdhere
Uday P. Khedker

abstract: The concept of an information flow path arising from the generalized theory of data flow analysis [21] is used to analyze the complexity of data flow analysis. The width (w) of a program flow graph with respect to a class of data flow problems is introduced as a measure of the complexity of round-robin iterative analysis. This provides the first known complexity result for round robin iterative analysis of bidirectional data flows commonly used in algorithms based on the suppression of partial redundancies [6, 7, 8, 9, 17, 18, 25]. We also show that width provides a better bound on the complexity of unidirectional data flows than the classical notion of depth.


title: A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML

authors:
Damien Doligez
Xavier Leroy

abstract: This paper presents the design and implementation of a “quasi real-time” garbage collector for Concurrent Caml Light, an implementation of ML with threads. This two-generation system combines a fast, asynchronous copying collector on the young generation with a non-disruptive concurrent marking collector on the old generation. This design crucially relies on the ML compile-time distinction between mutable and immutable objects.


title: A Sort Inference Algorithm for the Polyadic Pi-Calculus

abstract: In Milner's polyadic π-calculus there is a notion of sorts which is analogous to the notion of types in functional programming. As a well-typed program applies functions to arguments in a consistent way, a well-sorted process uses communication channels in a consistent way. An open problem is whether there is an algorithm to infer sorts in the π-calculus in the same way that types can be inferred in functional programming. Here we solve the problem by presenting an algorithm which infers the most general sorting for a process in the first-order calculus, and proving its correctness. The algorithm is similar in style to those used for Hindley-Milner type inference in functional languages.


title: Explicit Polymorphism and CPS Conversion

authors:
Robert Harper
Mark Lillibridge

abstract: We study the typing properties of CPS conversion for an extension of Fω with control operators. Two classes of evaluation strategies are considered, each with call-by-name and call-by-value variants. Under the “standard” strategies, constructor abstractions are values, and constructor applications can lead to non-trivial control effects. In contrast, the “ML-like” strategies evaluate beneath constructor abstractions, reflecting the usual interpretation of programs in languages based on implicit polymorphism. Three continuation passing style sub-languages are considered, one on which the standard strategies coincide, one on which the ML-like strategies coincide, and one on which all strategies coincide. Compositional, type-preserving CPS transformation algorithms are given for the standard strategies, resulting in terms on which all evaluation strategies coincide. This has as a corollary the soundness and termination of well-typed programs under the standard evaluation strategies. A similar result is obtained for the ML-like call-by-name strategy. In contrast, such results are obtained for the call-by-name strategy. In contrast, such results are obtained for the call-by value ML-like strategy only for a restricted sub-language in which constructor abstractions are limited to values.


title: Imperative Functional Programming

authors:
Simon L. Peyton Jones
Philip Wadler

abstract: We present a new model, based on monads, for performing input/output in a non-strict, purely functional language. It is composable, extensible, efficient, requires no extensions to the type system, and extends smoothly to incorporate mixed-language working and in-place array updates.

awards: Most Influential POPL Paper (awarded 2003)


title: Graph Types

authors:
Nils Klarlund
Michael I. Schwartzbach

abstract: Recursive data structures are abstractions of simple records and pointers. They impose a shape invariant, which is verified at compile-time and exploited to automatically generate code for building, copying, comparing, and traversing values without loss of efficiency. However, such values are always tree shaped, which is a major obstacle to practical use.We propose a notion of graph types, which allow common shapes, such as doubly-linked lists or threaded trees, to be expressed concisely and efficiently. We define regular languages of routing expressions to specify relative addresses of extra pointers in a canonical spanning tree. An efficient algorithm for computing such addresses is developed. We employ a second-order monadic logic to decide well-formedness of graph type specifications. This logic can also be used for automated reasoning about pointer structures.


title: Efficient Recursive Subtyping

authors:
Dexter Kozen
Jens Palsberg
Michael I. Schwartzbach

abstract: Subtyping in the presence of recursive types for the l-calculus was studied by Amadio and Cardelli in 1991 [1]. In that paper they showed that the problem of deciding whether one recursive type is a sub-type of another is decidable in exponential time.In this paper we give an O(n2) algorithm. Our algorithm is based on a simplification of the definition of the subtype relation, which allows us to reduce the problem to the emptiness problem for a certain finite automaton with quadratically many states.It is known that equality of recursive types and the covariant Bo¨hm order can be decided efficiently by means of finite automata. Our results extend the automata-theoretic approach to handle orderings based on contravariance.


title: Constructing Call Multigraphs Using Dependence Graphs

abstract: Article Constructing call multigraphs using dependence graphs Share on Author: Arun Lakhotia View Profile Authors Info & Claims POPL '93: Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesMarch 1993 Pages 273–284https://doi.org/10.1145/158511.158647Online:01 March 1993Publication History 22citation351DownloadsMetricsTotal Citations22Total Downloads351Last 12 Months7Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access


title: A Natural Semantics for Lazy Evaluation

abstract: We define an operational semantics for lazy evaluation which provides an accurate model for sharing. The only computational structure we introduce is a set of bindings which corresponds closely to a heap. The semantics is set at a considerably higher level of abstraction than operational semantics for particular abstract machines, so is more suitable for a variety of proofs. Furthermore, because a heap is explicitly modelled, the semantics provides a suitable framework for studies about space behaviour of terms under lazy evaluation.


title: Separating Stages in the Continuation-Passing Style Transformation

authors:
Julia L. Lawall
Olivier Danvy

abstract: The continuation-passing style (CPS) transformation is powerful but complex. Our thesis is that this transformation is in fact compound, and we set out to stage it. We factor the CPS transformation into several steps, separating aspects in each step: (1) Intermediate values are named; (2) Continuations are introduced; (3) Sequencing order is decided and administrative reductions are performed.


title: Quasi-Static Scoping: Sharing Variable Bindings Across Multiple Lexical Scopes

authors:
Shinn-Der Lee
Daniel P. Friedman

abstract: Static scoping embodies a strong encapsulation mechanism for hiding the details of program units. Yet, it does not allow the sharing of variable bindings (locations) across independent program units. Facilities such as module and object systems that require cross references of variables therefore must be added as special features. In this paper we present an alternative: quasi-static scoping. Quasi-static scoping is more flexible than static scoping, but has the same encapsulation mechanism. The user can control when and in what scope to resolve a quasi-static variable, i.e., to associate it with a variable binding. To demonstrate its versatility, we add quasi-static scoping to Scheme and show how to build the aforementioned facilities at the user-level. We also show that quasi-static scoping can be implemented efficiently.


title: Stratified Functional Programs and Computational Complexity

abstract: We develop two notions of stratified recur-1 introduction rence.The first is predicative recurrence, and is similar to


title: Polymorphism by Name for References and Continuations

abstract: This article investigates an ML-like language with byname semantics for polymorphism: polymorphic objects are not evaluated once for all at generalization time, but re-evaluated at each specialization. Unlike the standard ML semantics, the by-name semantics works well with polymorphic references and polymorphic continuations: the naive typing rules for references and for continuations are sound with respect to this semantics. Polymorphism by name leads to a better integration of these imperative features into the ML type discipline. Practical experience shows that it retains most of the efficiency and predictability of polymorphism by value.


title: A Constructive Logic of Multiple Subtyping

abstract: We show how a higher order logic, the calculus of constructions, can be used to give a simple, first principles treatment of record calculi, polymorphism, and subtyping. The development follows the constructive idiom of extracting implementations of equationally specified programs from proofs of their termination, with a logic for reasoning about programs, and a semantics that comes as a gratuity. In this framework, records are finitely specified functions where equality is decidable over the domain, with types that are a particular kind of logical assertion. By proving that a record specification satisfies its type, we can extract its implementation. While program extraction serves as a sort of compiler, proof normalization serves as an interpreter; the latter serves to ensure in some sense the coherence of the translation embedded in the former.


title: The 3 R's of Optimizing Constraint Logic Programs: Refinement, Removal and Reordering

authors:
Kim Marriott
Peter J. Stuckey

abstract: Central to constraint logic programming (CLP) languages is the notion of a global constraint solver which is queried to direct execution and to which constraints are monotonically added. We present a methodology for use in the compilation of CLP languages which is designed to reduce the overhead of the global constraint solver. This methododology is based on three optimizations. The first, refinement, involves adding new constraints, which in effect make information available earlier in the computation, guiding subsequent execution away from unprofitable choices. The second, removal, involves eliminating constraints from the solver when they are redundant. The last, reordering, involves moving constraint addition later and constraint removal earlier in the computation. Determining the applicability of each optimization requires sophisticated global analysis. These analyses are based on abstract interpretation and provide information about potential and definite interaction between constraints.


title: Array Data-Flow Analysis and its Use in Array Privatization

authors:
Dror E. Maydan
Saman P. Amarasinghe
Monica S. Lam

abstract: Data-flow analysis of scalar variables and data dependence analysis on array elements are two important program analyses used in optimizing and parallelizing compilers. Traditional data-flow analysis models accesses of array elements simply as accesses to the entire array, and is inadequate for parallelizing loops in array-based programs. On the other hand, data dependence analysis differentiates between different array elements but is flow-insensitive.


title: A Novel Framework of Register Allocation for Software Pipelining

authors:
Qi Ning
Guang R. Gao

abstract: Although software pipelining has been proposed as one of the most important loop scheduling methods, simultaneous scheduling and register allocation is less understood and remains an open problem [28]. The objective of this paper is to develop a unified algorithmic framework for concurrent scheduling and register allocation to support time-optimal software pipelining. A key intuition leading to this surprisingly simple formulation and its efficient solution is the association of maximum computation rate of a program graph with its critical cycles due to Reiter's pioneering work on Karp-Miller computation graphs [29]. In particular, our method generalizes the work by Callahan, Carr and Kennedy on scalar expansion[6], the work by Lam on modular variable expansion for software pipelined loops [20], and the work by Rau et al. on register allocation for modulo scheduled loops[28].


title: Type Checking Type Classes

authors:
Tobias Nipkow
Christian Prehofer

abstract: We study the type inference problem for a system with type classes as in the functional programming language Haskell. Type classes are an extension of ML-style polymorphism with overloading. We generalize Milner's work on polymorphism by introducing a separate context constraining the type variables in a typing judgement. This lead to simple type inference systems and algorithms which closely resemble those for ML. In particular we present a new unification algorithm which is an extension of syntactic unification with constraint solving. The existence of principal types follows from an analysis of this unification algorithm.


title: Relational Parametricity and Local Variables

authors:
Peter W. O'Hearn
Robert D. Tennent

abstract: J. C. Reynolds suggested that Strachey's intuitive concept of “parametric” (i.e., uniform) polymorphism is closely linked to representation independence, and used logical relations to formalize this principle in languages with type variables and user-defined types. Here, we use relational parametricity to address long-standing problems with the semantics of local-variable declarations, by showing that interactions between local and non-local entities satisfy certain relational criteria.


title: Call by Name, Assignment, and the Lambda Calculus

authors:
Martin Odersky
Dan Rabin
Paul Hudak

abstract: We define an extension of the call-by-name lambda calculus with additional constructs and reduction rules that represent mutable variables and assignments. The extended calculus has neither a concept of an explicit store nor a concept of evaluation order; nevertheless, we show that programs in the calculus can be implemented using a single-threaded store. We also show that the new calculus has the Church-Rosser property and that it is a conservative extension of classical lambda calculus with respect to operational equivalence; that is, all algebraic laws of the functional subset are preserved.


title: Semantics for Communication Primitives in an Polymorphic Language

authors:
Atsushi Ohori
Kazuhiko Kato

abstract: We propose a method to extend an ML-style polymorphic language with transparent communication primitives, and give their precise operational semantics. These primitives allow any polymorphic programs definable in ML to be used remotely in a manner completely transparent to the programmer. Furthermore, communicating programs may be based on different architecture and use different data representations.


title: Object-Oriented Programming without Recursive Types

authors:
Benjamin C. Pierce
David N. Turner

abstract: It is widely agreed that recursive types are inherent in the static typing of the essential mechanisms of object-oriented programming: encapsulation, message passing, subtyping, and inheritance. We demonstrate here that modeling object encapsulation in terms of existential types yields a substantially more straightforward explanation of these features in a simpler calculus without recursive types.


title: A Categorized Bibliography on Incremental Computation

authors:
G. Ramalingam
Thomas W. Reps

abstract: In many kinds of emnputatiomd contexts, modifications of the input data are to be processed at once so as to have immediate effect on the output. Because small changes in the input to a computation often cause only small changes in the outpu~ the challenge is to compute the new output incrementally by updating parts of the old outpu~ rather than by recomputing the entire output from scratch (as a “batch computation”)


title: Algebraic Reasoning and Completeness in Typed Languages

authors:
Jon G. Riecke
Ramesh Subrahmanyam

abstract: We consider the following problem in proving observational congruences in functional languages: given a call-by-name language based on the simply-typed λ-calculus with algebraic operations axiomatized by algebraic equations E, is the set of observational congruences between terms exactly those provable from (β), (η), and E? We find conditions for determining whether βηE-equational reasoning is complete for proving the observational congruences between such terms. We demonstrate the power and generality of the theorems by presenting a number of easy corollaries for particular algebras.


title: An Introduction to Logical Relations and Parametric Polymorphism - Tutorial

abstract: No abstract available.


title: Smartest Recompilation

authors:
Zhong Shao
Andrew W. Appel

abstract: To separately compile a program module in traditional statically-typed languages, one has to manually write down an import interface which explicitly specifies all the external symbols referenced in the module. Whenever the definitions of these external symbols are changed, the module has to be recompiled. In this paper, we present an algorithm which can automatically infer the “minimum” import interface for any module in languages based on the Damas-Milner type discipline (e.g., ML). By “minimum”, we mean that the interface specifies a set of assumptions (for external symbols) that are just enough to make the module type-check and compile. By compiling each module using its “minimum” import interface, we get a separate compilation method that can achieve the following optimal property: A compilation unit never needs to be recompiled unless its own implementation changes.


title: Computer Architectures and Programming Models for Scalable Parallel Computing

abstract: No abstract available.


title: Static Single Assignment for Explicitely Parallel Programs

authors:
Harini Srinivasan
James Hook
Michael Wolfe

abstract: We describe and prove algorithms to convert programs which use the Parallel Computing Forum Parallel Sections construct into Static Single Assignment (SSA) form. This proces allows compilers to apply classical scalar optimization algorithms to explicitly parallel programs. To do so, we must define what the concept of dominator and dominance frontier mean in parallel programs. We also describe how we extend SSA form to handle parallel updates and still preserve the SSA properties.


title: Specifying the Correctness of Binding-Time Analysis

abstract: Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for the incorporating flow analyses into verified compilers.


title: On the Orthogonality of Assignments and Procedures in Algol

authors:
Stephen Weeks
Matthias Felleisen

abstract: According to folklore, Algol is an “orthogonal” extension of a simple imperative programming language with a call-by-name functional language. The former contains assignments, branching constructs, and compound statements; the latter is based on the typed λ-calculus. In an attempt to formalize the claim of “orthogonality”, we define a simple version of Algol and an extended λ-calculus. The calculus includes the full β-rule and rules for the reduction of assignment statements and commands. It has the usual properties, e.g., it satisfies a Church-Rosser and Strong Normalization Theorem. In support of the claim that the imperative and functional components are orthogonal to each other, we show that the proofs of these theorems are combinations of separate Church-Rosser and Strong Normalization theorems for each sublanguage.


title: Automatic Generation and Management of Interprocedural Program Analyses

authors:
Kwangkeun Yi
Williams Ludwell Harrison III

abstract: We have designed and implemented an interprocedural program analyzer generator, called system Z. Our goal is to automate the generation and management of semantics-based interprocedural program analysis for a wide range of target languages.


title: Dominators, Super Blocks, and Program Coverage

abstract: In this paper we present techniques to find subsets of nodes of a flowgraph that satisfy the following property: A test set that exercises all nodes in a subset exercises all nodes in the flowgraph. Analogous techniques to find subsets of edges are also proposed. These techniques may be used to significantly reduce the cost of coverage testing of programs. A notion of a super block consisting of one or more basic blocks in that super block must be exercised by the same input. Dominator relationships among super blocks are used to identify a subset of the super blocks whose coverage implies that of all super blocks and, in turn, that of all basic blocks. Experiments with eight systems in the range of 1-75K lines of code show that, on the average, test cases targeted to cover just 29% of the basic blocks and 32% of the branches ensure 100% block and branch coverage, respectively.


title: Soft Typing with Conditional Types

authors:
Alexander Aiken
Edward L. Wimmers
T. K. Lakshman

abstract: We present a simple and powerful type inference method for dynamically typed languages where no type information is supplied by the user. Type inference is reduced to the problem of solvability of a system of type inclusion constraints over a type language that includes function types, constructor types, union, intersection, and recursive types, and conditional types. Conditional types enable us to analyze control flow using type inference, thus facilitating computation of accurate types. We demonstrate the power and practicality of the method with examples and performance results from an implementation.


title: A Needed Narrowing Strategy

authors:
Sergio Antoy
Rachid Echahed
Michael Hanus

abstract: Narrowing is the operational principle of languages that integrate functional and logic programming. We propose a notion of a needed narrowing step that, for inductively sequential rewrite systems, extends the Huet and Le´vy notion of a needed reduction step. We define a strategy, based on this notion, that computes only needed narrowing steps. Our strategy is sound and complete for a large class of rewrite systems, is optimal w.r.t. the cost measure that counts the number of distinct steps of a derivation, computes only independent unifiers, and is efficiently implemented by pattern matching.


title: CHOCOLATE: Calculi of Higher Order COmmunication and LAmbda TErms

abstract: We propose a general definition of higher-order process calculi, generalizing CHOCS [Tho89] and related calculi, and investigate its basic properties. We give sufficient conditions under which a calculus is finitely-branching and effective. We show that a suitable notion of higher-order bisimulation is a congruence for a subclass of higher-order calculi. We illustrate our definitions with a simple calculus strictly stronger than CHOCS.


title: Proving Concurrent Constraint Programs Correct

authors:
Frank S. de Boer
Maurizio Gabbrielli
Elena Marchiori
Catuscia Palamidessi

abstract: We develop a compositional proof-system for the partial correctness of concurrent constraint programs. Soundness and (relative) completeness of the system are proved with respect to a denotational semantics based on the notion of strongest postcondition. The strongest postcondition semantics provides a justification of the declarative nature of concurrent constraint programs, since it allows to view programs as theories in the specification logic.


title: Call Forwarding: A Simple Interprocedural Optimization Technique for Dynamically Typed Languages

authors:
Koenraad De Bosschere
Saumya K. Debray
David Gudeman
Sampath Kannan

abstract: This paper discusses call forwarding, a simple interprocedural optimization technique for dynamically typed languages. The basic idea behind the optimization is straightforward: find an ordering for the “entry actions” of a procedure, and generate multiple entry points for the procedure, so as to maximize the savings realized from different call sites bypassing different sets of entry actions. We show that the problem of computing optimal solutions to arbitrary call forwarding problems is NP-complete, and describe an efficient greedy algorithm for the problem. Experimental results indicate that (i) this algorithm is effective, in that the solutions produced are generally close to optimal; and (ii) the resulting optimization leads to significant performance improvements for a number of benchmarks tested.


title: Composing Tree Attributions

authors:
John Boyland
Susan L. Graham

abstract: Using the simple tree attributions described in this paper, attribute values can themselves be trees, enabling attribution to be used for tree transformations. Unlike higher-order attribute grammars, simple tree attributions have the property of descriptional composition, which allows a complex transformation to be built up from simpler ones, yet be executed efficiently. In contrast to other formalisms that admit descriptional composition, notably composable attribute grammars, simple tree attributions have the expressive power to handle remote references and recursive syntactic (tree-generating) functions, providing significantly more general forms of attribution and transformation.


title: Reducing Indirect Function call Overhead in C++ Programs

authors:
Brad Calder
Dirk Grunwald

abstract: Modern computer architectures increasingly depend on mechanisms that estimate future control flow decisions to increase performance. Mechanisms such as speculative execution and prefetching are becoming standard architectural mechanisms that rely on control flow prediction to prefetch and speculatively execute future instructions. At the same time, computer programmers are increasingly turning to object-oriented languages to increase their productivity. These languages commonly use run time dispatching to implement object polymorphism. Dispatching is usually implemented using an indirect function call, which presents challenges to existing control flow prediction techniques.


title: Decidable Bounded Quantification

authors:
Giuseppe Castagna
Benjamin C. Pierce

abstract: The standard formulation of bounded quantification, system F≤, is difficult to work with and lacks important syntactic properties, such as decidability. More tractable variants have been studied, but those studied so far either exclude significant classes of useful programs or lack a compelling semantics.


title: An Operational Framework for Value-Passing Processes

authors:
Rance Cleaveland
Daniel Yankelevich

abstract: This paper develops a semantic framework for concurrent languages with value passing. An operation analogous to substitution in the λ-calculus is given, and a semantics is given for a value-passing version of Milner's Calculus of Communicating Systems (CCS). An operational equivalence is then defined and shown to coincide with Milner's (early) bisimulation equivalence. We also show how semantics maybe given for languages with asynchronous communication primitives. In contrast with existing approaches to value passing, this semantics does not reduce data exchange to pure synchronization over (potentially infinite) families of ports indexed by data, and it avoids variable renamings that are not local to processes engaged in communication.


title: Combinations of Abstract Domains for Logic Programming

authors:
Agostino Cortesi
Baudouin Le Charlier
Pascal Van Hentenryck

abstract: Abstract interpretation [7] is a systematic methodology to design static program analysis which has been studied extensively in the logic programming community, because of the potential for optimizations in logic programming compilers and the sophistication of the analyses which require conceptual support. With the emergence of efficient generic abstract interpretation algorithms for logic programming, the main burden in building an analysis is the abstract domain which gives a safe approximation of the concrete domain of computation. However, accurate abstract domains for logic programming are often complex because of the variety of analyses to perform their interdependence, and the need to maintain structural information. The purpose of this paper is to propose conceptual and software support for the design of abstract domains. It contains two main contributions: the notion of open product and a generic pattern domain. The open product is a new way of combining abstract domains allowing each combined domain to benefit from information from the other components through the notions of queries and open operations. The open product is general-purpose and can be used for other programming paradigms as well. The generic pattern domain Pat (R)automatically upgrades a domain D with structural information yielding a more accurate domain Pat (D) without additional design or implementation cost. The two contributions are orthogonal and can be combined in various ways to obtain sophisticated domains while imposing minimal requirements on the designer. Both contributions are characterized theoretically and experimentally and were used to design very complex abstract domains such as PAT(OProp⊗OMode⊗OPS) which would be very difficult to design otherwise. On this last domain, designers need only contribute about 20% (about 3,400 lines) of the complete system (about 17,700 lines).


title: Memory Subsystem Performance of Programs Using Copying Garbage Collection

authors:
Amer Diwan
David Tarditi
J. Eliot B. Moss

abstract: Heap allocation with copying garbage collection is believed to have poor memory subsystem performance. We conducted a study of the memory subsystem performance of heap allocation for memory subsystems found on many machines. We found that many machines support heap allocation poorly. However, with the appropriate memory subsystem organization, heap allocation can have good memory subsystem performance.


title: Portable, Unobtrusive Garbage Collection for Multiprocessor Systems

authors:
Damien Doligez
Georges Gonthier

abstract: 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 environments where the registers of running processes are not readily accessible, without imposing any overhead on the elementary operations of loading a register or reading or initializing a field. Furthermore our collector never blocks running mutator processes except possibly on requests for free memory; in particular, updating a field or creating or marking or sweeping a heap object does not involve system-dependent synchronization primitives such as locks. We also provide support for process creation and deletion, and for managing an extensible heap of variable-sized objects.


title: The Revival Transformation

authors:
Lawrence Feigen
David Klappholz
Robert Casazza
Xing Xue

abstract: 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 of a (partially dead) definition by tightening its execution conditions without changing the set of uses which it reaches or the conditions under which it reaches each of them.


title: Representing Monads

abstract: 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 continuation-passing and direct style to one for continuation-passing vs. general “monadic” style. We further show that the composable-continuations construct can itself be represented using ordinary, non-composable first-class continuations and a single piece of state. Thus, in the presence of two specific computational effects - storage and escapes - any expressible monadic structure (e.g., nondeterminism as represented by the list monad) can be added as a purely definitional extension, without requiring a reinterpretation of the whole language. The paper includes an implementation of the construction (in Standard ML with some New Jersey extensions) and several examples.


title: The Typed Polymorphic Label-Selective lambda-Calculus

authors:
Jacques Garrigue
Hassan Aït-Kaci

abstract: 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-selective λ-calculus, a conservative extension of λ-calculus that uses a labeling of abstractions and applications to perform unordered currying. In other words, it enables some form of commutation between arguments. This improves program legibility, thanks to the presence of labels, and efficiency, thanks to argument commuting. In this paper, we propose a simply typed version of the calculus, then extend it to one with ML-like polymorphic types. For the latter calculus, we establish the existence of principal types and we give an algorithm to compute them. Thanks to the fact that label-selective λ-calculus is a conservative extension of λ-calculus by adding numeric labels to stand for argument positions, its polymorphic typing provides us with a keyword argument-passing extension of ML obviating the need of records. In this context, conventional ML syntax can be seen as a restriction of the more general keyword-oriented syntax limited to using only implicit positions instead of keywords.


title: Deriving Algorithms From Type Inference Systems: Application to Strictness Analysis

authors:
Chris Hankin
Daniel Le Métayer

abstract: 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 been investigated but the connection with efficient inference algorithms has been obscured. The contribution of this paper is twofold: first we show how to transform a program logic into an algorithm and, second, we introduce the notion of lazy types and show how to derive an efficient algorithm or strictness analysis.


title: A Type-Theoretic Approach to Higher-Order Modules with Sharing

authors:
Robert Harper
Mark Lillibridge

abstract: 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 interface. Experience has shown that fully opaque interfaces are awkward to use in practice since too much information is hidden, and that fully transparent interfaces lead to excessive interdependencies, creating problems for maintenance and separate compilation. The “sharing” specifications of Standard ML address this issue by allowing the programmer to specify equational relationships between types in separated modules, but are not expressive enough to allow the programmer complete control over the propagation of type information between modules.


title: A Generic Account of Continuation-Passing Styles

authors:
John Hatcliff
Olivier Danvy

abstract: 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 administrative reductions and inverse transformations.We establish generic formal connections between operational semantics and equational theories.Formal properties of transformations for specific evaluation orders follow as corollaries.Essentially, we factor transformations through Moggi's computational meta-language.Mapping A-terms into the met a-language captures computational properties (e.g., partiality, strictness) and evaluation order explicitly in both the term and the type structure of the meta-language.The CPS transformation is then obtained by applying a generic transformation from terms and types in the meta-language to CPS terms and types, based on a typed term representation of the continuation monad.We prove an adequacy property for the generic transformation and establish an equational correspondence between the meta-language and CPS terms.These generic results generalize Plotkin's seminal theorems, subsume more recent results, and enable new uses of CPS transformations and their inverses.We discuss how to apply these results to compilation.


title: Formally Optimal Boxing

authors:
Fritz Henglein
Jesper Jørgensen

abstract: 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/unboxing operations we axiomatize equationally the set of all explicitly boxed versions, called completions, of a given source program. In a two-stage process we give some of the equations a rewriting interpretation that captures eliminating boxing/unboxing operations without relying on a specific implementation or even semantics of the underlying language. The resulting reduction systems operate on congruence classes of completions defined by the remaining equations E, which can be understood as moving boxing/unboxing operations along data flow paths in the source program. We call a completion eopt formally optimal if every other completion for the same program (and at the same representation type) reduces to eopt under this two-stage reduction.


title: Combinatory Representation of Mobile Processes

authors:
Kohei Honda
Nobuko Yoshida

abstract: 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 seven atoms and fixed interaction rules, but with no notion of prefixing, is introduced, and is shown to be capable of representing input and output prefixes over arbitrary terms in a behaviourally correct way, just as SK-combinators are closed under functional abstraction without having it as a proper syntactic construct. The basic equational correspondence between concurrent combinators and a system of asynchronous mobile processes, as well as the embedding of the finite part of π-calculus in concurrent combinators, is proved. These results will hopefully serve as a cornerstone for further investigation of the theoretical as well as pragmatic possibilities of the presented construction.


title: A Type System for Prototyping Languages

authors:
Dinesh Katiyar
David C. Luckham
John C. Mitchell

abstract: 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 describe the main features of the type language, its intended use in a prototyping environment, and rationale for selected design decisions.


title: Manifest Types, Modules, and Separate Compilation

abstract: International audience


title: From Lambda-sigma to Lambda-upsilon a Journey Through Calculi of Explicit Substitutions

abstract: 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 of λ-terms.


title: Analyzing Logic Programs with Dynamic Scheduling

authors:
Kim Marriott
Maria J. García de la Banda
Manuel V. Hermenegildo

abstract: 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 dynamically “delayed” until their arguments are sufficiently instantiated to allow the call to run efficiently. Such dynamic scheduling has a significant cost. We give a framework for the global analysis of logic programming languages with dynamic scheduling and show that program analysis based on this framework supports optimizations which remove much of the overhead of dynamic scheduling.


title: Lazy Array Data-Flow Dependence Analysis

abstract: 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 analysis algorithm which exactly computes value-based dependence relations for program fragments in which all subscripts, loop bound and IF conditions are affine. Our algorithm also computes good affine approximations of dependence relations for non-affine program fragments. Actually, we do not know about any other algorithm which can compute better approximations.


title: A Staging Calculus and its Application to the Verification of Translators

abstract: 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 for confluence for terms in the calculus. The condition can be taken as a correctness criterion for translators that perform reductions in one stage leaving residual redexes over for subsequent computation stages. As an application of the theory, we verify the correctness of a macro expansion algorithm. The expansion algorithm is of some interest in its own right since it solves the problem of desired variable capture using only the familiar capture avoiding substitutions.


title: Higher-Order Concurrent Programs with Finite Communication Topology

authors:
Hanne Riis Nielson
Flemming Nielson

abstract: 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 given program may be very complex and therefore an efficient implementation may be facilitated by knowledge of the topology.


title: A Functional Theory of Local Names

abstract: λ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 core.


title: Multi-Pass Execution of Functional Logic Programs

abstract: 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 execution is divided into two phases: (1) construction of an incomplete proof tree, and (2) its decoration into a complete proof tree. The construction phase applies a modified SLD-resolution scheme, and the decoration phase a partial (multi-pass) traversal over the tree. The phase partition is generated by static analysis where data dependencies are extracted for the functional elements of the program. The method guarantees that all the functional terms of a program can be evaluated, and no dynamic groundness checks are needed.