- Sponsor:
- sigplan
No abstract available.
The program dependence graph and vectorization
Previous attempts at vectorizing programs written in a sequential high level language focused on converting control dependences to data dependences using a mechanism known as IF-conversion. After IF-conversion vector optimizations are performed on a ...
A rewriting semantics for program dependence graphs
Program dependence graphs are an important program representation technique for use in vectorization, parallelization and programming environments. We present a graph rewriting semantics for program dependence graphs and prove the equivalence between ...
Resolving circularity in attribute grammars with applications to data flow analysis (preliminary version)
Circular attribute grammars appear in many data flow analysis problems. As one way of making the notion useful, an automatic translation of circular attribute grammars to equivalent non-circular attribute grammars is presented. It is shown that for ...
Fast interprocedual alias analysis
We present a new algorithm for computing interprocedural aliases due to passing parameters by reference. This algorithm runs in O(N2+NE) time and, when combined with algorithms for alias-free, flow-insensitive data-flow problems, yields algorithms for ...
How to make ad-hoc polymorphism less ad hoc
This paper presents type classes, a new approach to ad-hoc polymorphism. Type classes permit overloading of arithmetic operators such as multiplication, and generalise the “eqtype variables” of Standard ML. Type classes extend the Hindley/Milner ...
Type checking records and variants in a natural extension of ML
Strongly typed languages with records may have inclusion rules so that records with more fields can be used instead of records with less fields. But these rules lead to a global treatment of record types as a special case. We solve this problem by ...
Extracting Ω's programs from proofs in the calculus of constructions
We define in this paper a notion of realizability for the Calculus of Constructions. The extracted programs are terms of the Calculus that do not contain dependent types. We introduce a distinction between informative and non-informative propositions. ...
Polymorphic unification and ML typing
We study the complexity of type inference for a core fragment of ML with lambda abstraction, function application, and the polymorphic let declaration. Our primary technical tool is the unification problem for a class of “polymorphic” type expressions. ...
Moded type systems for logic programming
Most of the theoretical work on the semantics of logic programs assumes an interpreter that provides a complete resolution procedure. In contrast, for reasons of efficiency, most logic programming languages are built around incomplete procedures. This ...
CLP and constraint abstraction
CLP*(D) is a class of constraint logic programming languages which incorporates the notion of abstraction. Predicates in CLP*(D) are (potentially) infinite rational trees which represent abstractions of constraint expressions. This view of predicates as ...
Fully abstract compositional semantics for logic programs
We propose a framework for discussing fully abstract compositional semantics, which exposes the interrelations between the choices of observables, compositions, and meanings. Every choice of observables and compositions determines a unique fully ...
A calculus of higher order communicating systems
In this paper we present A Calculus of Higher Order Communicating Systems. This calculus considers sending and receiving processes to be as fundamental as nondeterminism and parallel composition.
The calculus is an extension of CCS [Mil80] in the sense ...
A fully abstract trace model for dataflow networks
A dataflow network consists of nodes that communicate over perfect FIFO channels. For dataflow networks containing only deterministic nodes, a simple and elegant semantic model has been presented by Kahn. However, for nondeterministic networks, the ...
Efficient temporal reasoning (extended abstract)
There has been much interest in decision procedures for testing satisfiability (or validity) of formulae in various systems of Temporal Logic. This is due to the potential applications of such decision procedures to mechanical reasoning about ...
On the synthesis of a reactive module
We consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula (∀x) (∃y) A@@@@(x, y) is valid ...
Synthesis of concurrent systems with many similar sequential processes (extended abstract)
Methods for synthesizing concurrent programs from Temporal Logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson & Clarke [EC82] and Manna & Wolper [MW84]. An important advantage ...
The Modula–3 type system
This paper presents an overview of the programming language Modula-3, and a more detailed description of its type system.
Dynamic typing in a statically-typed language
Statically-typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type-consistency checks are performed at runtime. However, ...
Relating models of polymorphism
A new general notion of model for the polymorphic lambda calculus based on the simple idea of a universe, is proposed. Although impossible in nonconstructive set theory, the notion is unproblematic for constructive sets, yields completeness and ...
Generalized conjunctive types
The definitions of Conjunctive types and their subtype relation, as introduced by Coppo-Dezani, are extended to consider the conjunction as a partial mapping from pairs of types to types, and the subtype relation as a relation between finite sets of ...
Rewrite, rewrite, rewrite, rewrite, rewrite...
The theory of term rewriting systems has important applications in abstract data type specifications and functional programming languages. We begin here a study of properties of systems that are not necessarily terminating, but allow for infinite ...
Partial order programming (extended abstract)
We introduce a programming paradigm in which statements are constraints over partial orders. A partial order programming problem has the form minimize u subject to u1 ⊒ v1, u2 ⊒ v2, ··· where u is the goal, and u1 ⊒ v1, u2 ⊒ v2, ··· is a collection of ...
Temporal logic programming is complete and expressive
This paper addresses semantic and expressiveness issues for temporal logic programming and in particular for the TEMPLOG language proposed by Abadi and Manna. Two equivalent formulations of TEMPLOG's declarative semantics are given: in terms of a ...
Realistic compilation by program transformation (detailed summary)
Using concepts from denotational semantics, we have produced a very simple compiler that can be used to compile standard programming languages and produces object code as efficient as that of production compilers. The compiler is based entirely on ...
Continuation-passing, closure-passing style
We implemented a continuation-passing style (CPS) code generator for ML. Our CPS language is represented as an ML datatype in which all functions are named and most kinds of ill-formed expressions are impossible. We separate the code generation into ...
Copy elimination in functional languages
Copy elimination is an important optimization for compiling functional languages. Copies arise because these languages lack the concepts of state and variable; hence updating an object involves a copy in a naive implementation. Copies are also possible ...
Unified algebras and modules
This paper concerns the algebraic specification of abstract data types. It introduces and motivates the recently-developed framework of unified algebras, and provides a practical notation for their modular specification. It also compares unified ...
Bisimulation through probabilistic testing (preliminary report)
We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm with ...
Index Terms
- Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Recommendations
Acceptance Rates
Year | Submitted | Accepted | Rate |
---|---|---|---|
POPL '15 | 227 | 52 | 23% |
POPL '14 | 220 | 51 | 23% |
POPL '04 | 176 | 29 | 16% |
POPL '03 | 126 | 24 | 19% |
POPL '02 | 128 | 28 | 22% |
POPL '01 | 126 | 24 | 19% |
POPL '00 | 151 | 30 | 20% |
POPL '99 | 136 | 24 | 18% |
POPL '98 | 175 | 32 | 18% |
POPL '97 | 225 | 36 | 16% |
POPL '96 | 148 | 34 | 23% |
POPL '94 | 173 | 39 | 23% |
POPL '93 | 199 | 39 | 20% |
POPL '92 | 204 | 30 | 15% |
POPL '91 | 152 | 31 | 20% |
POPL '89 | 191 | 30 | 16% |
POPL '88 | 177 | 28 | 16% |
POPL '87 | 108 | 29 | 27% |
POPL '83 | 170 | 28 | 16% |
POPL '82 | 121 | 38 | 31% |
POPL '81 | 121 | 24 | 20% |
POPL '79 | 146 | 27 | 18% |
POPL '78 | 135 | 27 | 20% |
POPL '77 | 105 | 25 | 24% |
POPL '76 | 90 | 20 | 22% |
POPL '75 | 100 | 23 | 23% |
POPL '73 | 100 | 22 | 22% |
Overall | 4,130 | 824 | 20% |