Last update:
Sat Jan 18 06:29:21 MST 2025
Gary Lindstrom Backtracking in a Generalized Control
Setting . . . . . . . . . . . . . . . . 8--26
Robert B. K. Dewar and
Arthur Grand and
Ssu-Cheng Liu and
Jacob T. Schwartz and
Edmond Schonberg Programming by Refinement, as
Exemplified by the SETL Representation
Sublanguage . . . . . . . . . . . . . . 27--49
Richard L. Sites The Compilation of Loop Induction
Expressions . . . . . . . . . . . . . . 50--57
Carlo Ghezzi and
Dino Mandrioli Incremental Parsing . . . . . . . . . . 58--70
Edward L. Robertson Code Generation and Storage Allocation
for Machines with Span-Dependent
Instructions . . . . . . . . . . . . . . 71--83
Leslie Lamport A New Approach to Proving the
Correctness of Multiprocess Programs . . 84--97
Robert L. Constable and
James E. Donahue A Hierarchical Approach to Formal
Semantics With Application to the
Definition of PL/CS . . . . . . . . . . 98--114
David S. Wise Morris's Garbage Compaction Algorithm
Restores Reference Counts . . . . . . . 115--120
Thomas Lengauer and
Robert Endre Tarjan A Fast Algorithm for Finding Dominators
in a Flowgraph . . . . . . . . . . . . . 121--141
Ken Kennedy and
Jayashree Ramanathan A Deterministic Attribute Grammar
Evaluator Based on Dynamic Scheduling 142--160
Kenneth E. Iverson Operators . . . . . . . . . . . . . . . 161--176
R. H. Perrott A Language for Array and Vector
Processors . . . . . . . . . . . . . . . 177--195
N. S. Prywes and
Amir Pnueli and
S. Shastry Use of a Nonprocedural Specification
Language and Associated Program
Generator in Software Development . . . 196--217
Richard B. Kieburtz and
Abraham Silberschatz Comments on ``Communicating Sequential
Processes'' . . . . . . . . . . . . . . 218--225
David C. Luckham and
Norihisa Suzuki Verification of Array, Record, and
Pointer Operations in Pascal . . . . . . 226--244
Greg Nelson and
Derek C. Oppen Simplification by Cooperating Decision
Procedures . . . . . . . . . . . . . . . 245--257
David Gries Is Sometimes Ever Better Than Alway? . . 258--265
Daniel G. Bobrow and
Douglas W. Clark Compact Encodings of List Structure . . 266--286
Eric Beyer and
Peter Buneman A Space Efficient Dynamic Allocation
Algorithm for Queuing Messages . . . . . 287--294
Kou-Chung Tai Noncanonical SLR(1) Grammars . . . . . . 295--320
David Harel And/Or Programs: a New Approach to
Structured Programming . . . . . . . . . 1--17
Ajit B. Pai and
Richard B. Kieburtz Global Context Recovery: a New Strategy
for Syntactic Error Recovery by
Table-Drive Parsers . . . . . . . . . . 18--41
Nissim Francez Distributed Termination . . . . . . . . 42--55
Gregory R. Andrews and
Richard P. Reitman An Axiomatic Approach to Information
Flow in Programs . . . . . . . . . . . . 56--76
Christos H. Papadimitriou and
Philip A. Bernstein On the Performance of Balanced Hashing
Functions When the Keys Are Not
Equiprobable . . . . . . . . . . . . . . 77--89
Zohar Manna and
Richard Waldinger A Deductive Approach to Program
Synthesis . . . . . . . . . . . . . . . 90--121
D. B. Arnold and
M. R. Sleep Uniform Random Generation of Balanced
Parenthesis Strings . . . . . . . . . . 122--128
Douglas Comer A Note on Median Split Trees . . . . . . 129--133
Leslie Lamport Corrigendum: ``A New Approach to Proving
the Correctness of Multiprocess
Programs'' . . . . . . . . . . . . . . . 134--134
Peter J. L. Wallis External Representations of Objects of
User-Defined Type . . . . . . . . . . . 137--152
Ralph E. Griswold and
David R. Hanson An Alternative to the Use of Patterns in
String Processing . . . . . . . . . . . 153--172
R. G. G. Cattell Automatic Derivation of Code Generators
from Machine Descriptions . . . . . . . 173--190
Jack W. Davidson and
Christopher W. Fraser The Design and Application of a
Retargetable Peephole Optimizer . . . . 191--202
Charles N. Fischer On Parsing and Compiling Arithmetic
Expressions on Vector Computers . . . . 203--224
David C. Luckham and
W. Polak Ada exception handling: an axiomatic
approach . . . . . . . . . . . . . . . . 225--233
Arthur Bernstein Output Guards and Nondeterminism in
``Communicating Sequential Processes'' 234--238
Perng-Ti Ma and
T. G. Lewis Design of a Machine-Independent
Optimizing System for Emulator
Development . . . . . . . . . . . . . . 239--262
Daniel G. Bobrow Managing Reentrant Structures Using
Reference Counts . . . . . . . . . . . . 269--273
Bruce W. Leverett and
Thomas G. Szymanski Chaining Span-Dependent Jump
Instructions . . . . . . . . . . . . . . 274--289
Hanan Samet A Coroutine Approach to Parsing . . . . 290--306
W. E. Howden Applicability of Software Validation
Techniques to Scientific Programs . . . 307--320
Manfred Broy and
Bernd Krieg-Brückner Derivation of Invariant Assertions
During Program Development by
Transformation . . . . . . . . . . . . . 321--337
Edmund Melson Clarke, Jr. Synthesis of Resource Invariants for
Concurrent Programs . . . . . . . . . . 338--358
Krzysztof R. Apt and
Nissim Francez and
Willem P. de Roever A Proof System for Communicating
Sequential Processes . . . . . . . . . . 359--385
Marco R. Casanova and
Phillip A. Bernstein A Formal System for Reasoning about
Programs Accessing a Relational Database 386--414
Susan L. Graham and
Michael A. Harrison and
Walter L. Ruzzo An Improved Context-Free Recognizer . . 415--462
Nissim Francez Corrigendum: ``Distributed Termination'' 463--463
Dereck C. Oppen Prettyprinting . . . . . . . . . . . . . 465--483
Jacob T. Schwartz Ultracomputers . . . . . . . . . . . . . 484--521
George W. Ernst and
William F. Ogden Specification of Abstract Data Types in
Modula . . . . . . . . . . . . . . . . . 522--543
Carl E. Landwehr An Abstract Type for Statistics
Collection in Simula . . . . . . . . . . 544--563
David Gries and
Gary Levin Assignment and Procedure Call Proof
Rules . . . . . . . . . . . . . . . . . 564--579
B. M. E. Moret and
M. G. Thomason and
R. C. Gonzalez The Activity of a Variable and Its
Relation to Decision Trees . . . . . . . 580--595
J. Steensgaard-Madsen A Statement-Oriented Approach to Data
Abstraction . . . . . . . . . . . . . . 1--10
F. André and
J. P. Banatre and
J. P. Routeau A Multiprocessing Approach to
Compile-Time Symbol Resolution . . . . . 11--23
Otto C. Juelich and
Clinton R. Foulk Compilation of Acyclic Smooth Programs
for Parallel Execution . . . . . . . . . 24--48
Dale H. Grit and
Rex L. Page Deleting Irrelevant Tasks in an
Expression-Oriented Multiprocessor
System . . . . . . . . . . . . . . . . . 49--59
Bent Bruun Kristensen and
Ole Lehrmann Madsen Methods for Computing LALR$ (k) $
Lookahead . . . . . . . . . . . . . . . 60--82
Wilf R. LaLonde and
Jim des Rivieres Handling Operator Precedence in
Arithmetic Expressions with Tree
Transformations . . . . . . . . . . . . 83--103
Jayadev Misra An Exercise in Program Explanation . . . 104--109
Jack W. Davidson and
Christopher W. Fraser Corrigendum: ``The Design and
Application of a Retargetable Peephole
Optimizer'' . . . . . . . . . . . . . . 110--110
Peter J. L. Wallis Corrigendum: ``External Representations
of Objects of User-Defined Type'' . . . 111--111
C. Mohan Technical Correspondence: On Francez's
``Distributed Termination'' . . . . . . 112--112
N. Francez Technical Correspondence: Reply from
Francez . . . . . . . . . . . . . . . . 112--113
Christopher W. Fraser and
A. A. Lopez Editing Data Structures . . . . . . . . 115--125
Edmond Schonberg and
Jacob T. Schwartz and
Micha Sharir An Automatic Technique for Selection of
Data Structures in SETL Programs . . . . 126--143
Ralph E. Griswold and
David R. Hanson and
John T. Korb Generators in Icon . . . . . . . . . . . 144--161
David R. Hanson Algorithm 568. PDS --- a Portable
Directory System . . . . . . . . . . . . 162--167
Wilf R. LaLonde The Construction of Stack-Controlling LR
Parsers for Regular Right Part Grammars 168--206
John Gannon and
Paul McMullin and
Richard Hamlet Data Abstraction, Implementation,
Specification, and Testing . . . . . . . 211--223
Jan van den Bos and
R. Plasmeijer and
Jan W. M. Stroet Process Communication Based on Input
Specifications . . . . . . . . . . . . . 224--250
Martin Rem Associons: a Program Notation with
Tuples Instead of Variables . . . . . . 251--262
Gary Lindstrom and
Mary Lou Soffa Referencing and Retention in
Block-Structured Coroutines . . . . . . 263--292
J. A. Barnden Nonsequentiality and Concrete Activity
Phases in Discrete-Event Simulation
Languages . . . . . . . . . . . . . . . 293--317
S. O. Anderson and
R. C. Backhouse Locally Least-Cost Error Recovery in
Early's Algorithm . . . . . . . . . . . 318--347
Alan Borning The Programming Language Aspects of
ThingLab, a Constraint-Oriented
Simulation Laboratory . . . . . . . . . 353--387
Medhi Jazayeri and
Diane Pozefsky Space-Efficient Storage Management in an
Attribute Grammar Evaluator . . . . . . 388--404
Gregory R. Andrews Synchronizing Resources . . . . . . . . 405--430
Krzysztof R. Apt Ten Years of Hoare's Logic: a Survey ---
Part I . . . . . . . . . . . . . . . . . 431--483
Irene Greif and
Albert R. Meyer Specifying the Semantics of while
Programs: a Tutorial and Critique of a
Paper by Hoare and Lauer . . . . . . . . 484--507
Wilfred J. Hansen A Cost Model for the Internal
Organization of B$^+$-Tree Nodes . . . . 508--532
Martin S. Feather A System for Assisting Program
Transformation . . . . . . . . . . . . . 1--20
Andrew S. Tanenbaum and
Hans van Staveren and
Johan W. Stevenson Using Peephole Optimization on
Intermediate Code . . . . . . . . . . . 21--36
Jayadev Misra and
K. M. Chandy Termination Detection of Diffusing
Computations in Communicating Sequential
Processes . . . . . . . . . . . . . . . 37--43
James R. McGraw The VAL Language: Description and
Analysis . . . . . . . . . . . . . . . . 44--82
Christoph M. Hoffman and
Michael J. O'Donnell Programming with Equations . . . . . . . 83--112
M. Howard Williams A Flexible Notation for Syntactic
Definitions . . . . . . . . . . . . . . 113--119
John R. Ellis Technical Correspondence: On
Steensgaard-Madsen's ``A
Statement-Oriented Approach to Data
Abstraction'' . . . . . . . . . . . . . 120--122
J. Steensgaard-Madsen Technical Correspondence:
Steensgaard-Madsen's reply . . . . . . . 122--123
Fred B. Schneider Synchronization in Distributed Programs 125--148
Richard C. Holt and
J. R. Cordy and
David B. Wortman An Introduction to S/SL: Syntax/Semantic
Language . . . . . . . . . . . . . . . . 149--178
Eljas Soisalon-Soininen Inessential Error Entries and Their Use
in LR Parser Optimization . . . . . . . 179--195
Micha Sharir Some Observations Concerning Formal
Differentiation of Set Theoretic
Expressions . . . . . . . . . . . . . . 196--225
C. S. Wetherell Error Data Values in the Data-Flow
Language VAL . . . . . . . . . . . . . . 226--238
Richard J. Fateman High-Level Language Implications of the
Proposed IEEE Floating-Point Standard 239--257
Alberto Martelli and
Ugo Montanari An Efficient Unification Algorithm . . . 258--282
E. A. Ashcroft and
W. W. Wadge \bf R$_{\! \! \! \mbox {\raisebox
{.5ex}{\tiny /}}}$ for Semantics . . . . 283--294
J. Arsac and
Y. Kodratoff Some Techniques for Recursion Removal
from Recursive Functions . . . . . . . . 295--322
John L. Hennessy Symbolic Debugging of Optimized Code . . 323--344
Paolo Sipala Compact Storage of Binary Trees . . . . 345--361
Manfred Broy and
Peter Pepper Combining Algebraic and Algorithmic
Reasoning: An Approach to the
Schorr--Waite Algorithm . . . . . . . . 362--381
Leslie Lamport and
Robert Shostak and
Marshall Pease The Byzantine Generals Problem . . . . . 382--401
Robert Paige and
Shaye Koenig Finite Differencing of Computable
Expressions . . . . . . . . . . . . . . 402--454
Susan Owicki and
Leslie Lamport Proving Liveness Properties of
Concurrent Programs . . . . . . . . . . 455--495
Mitchell Wand Deriving Target Code as a Representation
of Continuation Semantics . . . . . . . 496--517
Fred T. Krogh ACM Algorithms Policy . . . . . . . . . 518--521
Anonymous Information for Authors . . . . . . . . 522--525
Maurice P. Herlihy and
Barbara Liskov A Value Transmission Method for Abstract
Data Types . . . . . . . . . . . . . . . 527--551
Richard C. Holt and
David B. Wortman A Model for Implementing Euclid Modules
and Prototypes . . . . . . . . . . . . . 552--562
Ralph E. Griswold The Evaluation of Expressions in Icon 563--584
J. Gergeron and
A. Dubuque A Structured APL System . . . . . . . . 585--600
T. P. Baker A One-Pass Algorithm for Overload
Resolution in Ada . . . . . . . . . . . 601--614
Frank DeRemer and
Thomas Pennello Efficient Computation of LALR(1)
Look-Ahead Sets . . . . . . . . . . . . 615--649
Robert B. K. Dewar and
Micha Sharir and
Elia Weixelbaum Transformational Derivation of a Garbage
Collection Algorithm . . . . . . . . . . 650--667
H. J. Boom A Weaker Precondition for Loops . . . . 668--677
Jayadev Misra and
K. M. Chandy A Distributed Graph Algorithm: Knot
Detection . . . . . . . . . . . . . . . 678--686
William R. Mallgren Formal Specification of Graphic Data
Types . . . . . . . . . . . . . . . . . 687--710
J. W. Thatcher and
E. G. Wagner and
J. B. Wright Data Type Specification:
Parameterization and the Power of
Specification Techniques . . . . . . . . 711--732
John H. Williams On the Development of the Algebra of
Functional Programs . . . . . . . . . . 733--757
Gary L. Peterson An $ O(n \log {n}) $ Unidirectional
Algorithm for the Circular Extrema
Problem . . . . . . . . . . . . . . . . 758--762
Philip Merlin and
Gregor V. Bochmann On the Construction of Submodule
Specifications and Communication
Protocols . . . . . . . . . . . . . . . 1--25
Stefan M. Freudenberger and
Jacob T. Schwartz and
Micha Sharir Experience with the SETL Optimizer . . . 26--45
Gary L. Peterson Concurrent Reading While Writing . . . . 46--55
Gary L. Peterson A New Solution to Lamport's Concurrent
Programming Problem Using Small Shared
Variables . . . . . . . . . . . . . . . 56--65
R. G. Gallager and
P. A. Humblet and
P. M. Spira A Distributed Algorithm for
Minimum-Weight Spanning Trees . . . . . 66--77
Richard B. Kieburtz and
Abraham Silberschatz Access-Right Expressions . . . . . . . . 78--96
Samuel Kamin Final Data Types and Their Specification 97--121
Peter B. Henderson Technical Correspondence: On LaLonde and
des Rivieres' ``Handling Operator
Precedence in Arithmetic Expressions
with Tree Transformations'' . . . . . . 122--122
Wilf R. LaLonde Technical Correspondence: LaLonde's
Reply . . . . . . . . . . . . . . . . . 122--122
Steven P. Reiss Generation of Compiler Symbol Processing
Mechanisms from Specifications . . . . . 127--163
Allan Gottlieb and
Boris D. Lubachevsky and
Larry Rudolph Basic Techniques for the Efficient
Coordination of Very Large Numbers of
Cooperating Sequential Processors . . . 164--189
Leslie Lamport Specifying Concurrent Program Modules 190--222
G. N. Buckley and
Abraham Silberschatz An Effective Implementation for the
Generalized Input-Output Construct of
CSP . . . . . . . . . . . . . . . . . . 223--235
B. Maher and
D. H. Sleeman Automatic Program Improvement: Variable
Usage Transformations . . . . . . . . . 236--264
Norman H. Cohen Eliminating Redundant Recursive Calls 265--299
Eliezer Dekel and
Sartaj Sahni Parallel Generation of Postfix and Tree
Forms . . . . . . . . . . . . . . . . . 300--317
Harald Gazinger Parameterized Specifications: Parameter
Passing and Implementation with Respect
to Observability . . . . . . . . . . . . 318--354
Richard A. DeMillo Guest Editor's Introduction . . . . . . 355--355
Sergiu Hart and
Micha Sharir and
Amir Pnueli Termination of Probabilistic Concurrent
Program . . . . . . . . . . . . . . . . 356--380
Barbara Liskov and
Robert Scheifler Guardians and Actions: Linguistic
Support for Robust, Distributed Programs 381--404
Richard J. Lipton and
Jacobo Valdes and
Gopalakrishnan Vijayen and
Stephen C. Notth and
Robert Sedgewick VLSI Layout as Programming . . . . . . . 405--421
John L. Hennessy and
Thomas Gross Postpass Code Optimization of Pipeline
Constraints . . . . . . . . . . . . . . 422--448
Thomas Reps and
Tim Teitelbaum and
Alan Demers Incremental Context-Dependent Analysis
for Language-Based Editors . . . . . . . 449--477
Robert Giegerich A Formal Framework for the Derivation of
Machine-Specific Optimizers . . . . . . 478--498
Steven Pemberton Technical Correspondence: On Tanenbaum,
van Staveren, and Stevenson's ``Using
Peephole Optimization on Intermediate
Code'' . . . . . . . . . . . . . . . . . 499--499
Andrew S. Tanenbaum Technical Correspondence: Tanenbaum's
Reply . . . . . . . . . . . . . . . . . 499--500
Abha Moitra Technical Correspondence: On Apt,
Francez, and de Roever's ``A Proof
System for Communicating Sequential
Processes'' . . . . . . . . . . . . . . 500--501
F. T. Krogh ACM Algorithms Policy . . . . . . . . . 502--505
Anonymous Information for Authors . . . . . . . . 506--509
Richard C. Waters User Format Control in a Lisp
Prettyprinter . . . . . . . . . . . . . 513--531
Jacques Cohen and
Alexandru Nicolau Comparison of Compacting Algorithms for
Garbage Collection . . . . . . . . . . . 532--553
Ravi Sethi Control Flow Aspects of
Semantics-Directed Compiling . . . . . . 554--595
C. B. Jones Tentative Steps Toward a Development
Method for Interfering Programs . . . . 596--619
Marty Ossefort Correctness Proofs of Communicating
Processes: Three Illustrative Examples
from the Literature . . . . . . . . . . 620--640
Elaine J. Weyuker Assessing Test Data Adequacy through
Program Inference . . . . . . . . . . . 641--655
Seppo Sippu and
Eljas Soisalon-Soininen A Syntax-Error-Handling Technique and
Its Experimental Analysis . . . . . . . 656--679
James E. Archer, Jr. and
Richard Conway and
Fred B. Schneider User Recovery and Reversal in
Interactive Systems . . . . . . . . . . 1--19
Robert D. Cameron and
M. Robert Ito Grammar-Based Definition of
Metaprogramming Systems . . . . . . . . 20--54
L. Colussi Recursion As an Effective Step in
Program Development . . . . . . . . . . 55--67
Zohar Manna and
Pierre Wolper Synthesis of Communicating Processes
from Temporal Logic Specifications . . . 68--93
Robert L. Constable and
Daniel R. Zlatin The Type Theory of PL/CV3 . . . . . . . 94--117
Arie Kaufman Tailored-List and Recombination-Delaying
Buddy Systems . . . . . . . . . . . . . 118--125
William F. Appelbe and
A. P. Ravn Encapsulation Constructs in Systems
Programming Languages . . . . . . . . . 129--158
F. Warren Burton Annotations to Control Parallelism and
Reduction Order in the Distributed
Evaluation of Functional Programs . . . 159--174
M. Elizabeth C. Hull and
R. M. McKeag Communicating Sequential Processes for
Centralized and Distributed Operating
System Design . . . . . . . . . . . . . 175--191
Roland Backhouse Global Data Flow Analysis Problems
Arising in Locally Least-Cost Error
Recovery . . . . . . . . . . . . . . . . 192--214
John H. Reif and
Paul G. Spirakis Real-Time Synchronization of
Interprocess Communications . . . . . . 215--238
Richard Alan Karp Proving Failure-Free Properties of
Concurrent Systems Using Temporal Logic 239--253
Leslie Lamport Using Time Instead of Timeout for
Fault-Tolerant Distributed Systems . . . 254--280
Leslie Lamport and
Fred B. Schneider The ``Hoare Logic'' of CSP, and All That 281--296
Timothy A. Budd An APL Compiler for a Vector Processor 297--313
Richard F. Hobson A Directly Executable Encoding for APL 314--332
Mordechai Ben-Ari Algorithms for On-the-fly Garbage
Collection . . . . . . . . . . . . . . . 333--344
Takuya Katayama Translation of Attribute Grammars into
Procedures . . . . . . . . . . . . . . . 345--369
Krzysztof R. Apt and
Nissem Francez Modeling the Distributed Termination
Convention of CSP . . . . . . . . . . . 370--379
E. Korach and
D. Rotem and
N. Santoro Distributed Algorithms for Finding
Centers and Medians in Networks . . . . 380--401
Richard D. Schlichting and
Fred B. Schneider Using Message Passing for Distributed
Programming: Proof Rules and Disciplines 402--431
Wilf R. LaLonde Technical Correspondence: Comments on
Soisalon-Soininen's ``Inessential Error
Entries and Their Use in LR Parser
Optimization'' . . . . . . . . . . . . . 432--439
F. T. Krogh ACM Algorithms Policy . . . . . . . . . 440--443
Anonymous Information for Authors . . . . . . . . 444--447
Robert I. Winner Unassigned Objects . . . . . . . . . . . 449--467
Franco Turini Magma2: a Language Oriented toward
Experiments in Control . . . . . . . . . 468--486
R. S. Bird The Promotion and Accumulation
Strategies in Transformational
Programming . . . . . . . . . . . . . . 487--504
Jack W. Davidson and
Christopher W. Fraser Code Selection through Object Code
Optimization . . . . . . . . . . . . . . 505--526
M. V. S. Ramanath and
Marvin Solomon Jump Minimization in Linear Time . . . . 527--545
Peter Dencker and
Karl Dürre and
Johannes Heuft Optimization of Parser Tables for
Portable Compilers . . . . . . . . . . . 546--572
Naftaly H. Minsky Selective and Locally Controlled
Transport of Privileges . . . . . . . . 573--602
Michael Georgeff Transformations and Reduction Strategies
for Typed Lambda Expressions . . . . . . 603--631
K. M. Chandy and
Jayadev Misra The Drinking Philosopher's Problem . . . 632--646
N. Soundararajan Axiomatic Semantics of Communicating
Sequential Processes . . . . . . . . . . 647--662
David Barstow On Convergence Toward a Database of
Program Transformations . . . . . . . . 1--9
Pamela Zave A Distributed Alternative to
Finite-State-Machine Specifications . . 10--36
Jean-François Bergeretti and
Bernard A. Carré Information-Flow and Data-Flow Analysis
of while-Programs . . . . . . . . . . . 37--61
David R. Fuchs and
Donald E. Knuth Optimal Prepaging and Font Caching . . . 62--79
David Gelernter Generative Communication in Linda . . . 80--112
Joseph L. Bates and
Robert L. Constable Proofs as Programs . . . . . . . . . . . 113--136
Douglas D. Dunlop and
Victor R. Basili Generalizing Specifications for
Uniformly Implemented Loops . . . . . . 137--158
Joseph C. H. Park and
K. M. Choe and
C. H. Chang A New Analysis of LALR Formalisms . . . 159--175
D. Wall and
A. Srivastava and
F. Templin Technical Correspondence: a Note on
Hennessy's ``Symbolic Debugging of
Optimized Code'' . . . . . . . . . . . . 176--181
Jan Heering and
Paul Klint Towards Monolingual Programming
Environments . . . . . . . . . . . . . . 183--213
Shaula Yemini and
Daniel M. Berry A Modular Verifiable Exception-Handling
Mechanism . . . . . . . . . . . . . . . 214--243
William Weihl and
Barbara Liskov Implementation of Resilient, Atomic Data
Types . . . . . . . . . . . . . . . . . 244--269
George J. Milne CIRCAL and the representation of
communication, concurrency, and time . . 270--298
David A. Schmidt Detecting Global Variables in
Denotational Specifications . . . . . . 299--310
Keshav Pingali and
Arvind Efficient Demand-Driven Evaluation. Part
1 . . . . . . . . . . . . . . . . . . . 311--333
Giuseppina C. Gini and
Maria L. Gini Dealing with World-Model-Based Programs 334--347
Ilan Bar-On and
Uzi Vishkin Optimal Parallel Generation of a
Computation Tree Form . . . . . . . . . 348--357
Flemming Nielson Program Transformations in a
Denotational Setting . . . . . . . . . . 359--379
George S. Avrunin and
Jack C. Wileden Describing and Analyzing Distributed
Software System Designs . . . . . . . . 380--403
David R. Jefferson Virtual Time . . . . . . . . . . . . . . 404--425
James Donahue and
Alan Demers Data Types Are Values . . . . . . . . . 426--445
Nachum Dershowitz Program Abstraction and Instantiation 446--477
Helmut Richter Noncorrecting Syntax Error Recovery . . 478--489
R. S. Bird Addendum: ``The Promotion and
Accumulation Strategies in
Transformational Programming'' . . . . . 490--492
F. T. Krogh ACM Algorithms Policy . . . . . . . . . 493--496
Anonymous Information for Authors . . . . . . . . 497--500
Robert H. Halstead, Jr. Multilisp: A Language for Concurrent
Symbolic Computation . . . . . . . . . . 501--538
Malcolm P. Atkinson and
Ronald Morrison Procedures as Persistent Data Objects 539--559
Mahadevan Ganapathi and
Charles N. Fischer Affix Grammar Driven Code Generation . . 560--599
Robert P. Nix Editing by Example . . . . . . . . . . . 600--621
Nissim Francez and
Shaula A. Yemini Symmetric Intertask Communication . . . 622--636
Hans-Juergen Boehm Side Effects and Aliasing Can Have
Simple Axiomatic Descriptions . . . . . 637--655
Arie de Bruin and
Wim Böhm The Denotational Semantics of Dynamic
Networks of Processes . . . . . . . . . 656--679
Norman H. Cohen A note on Cohen's ``Eliminating
Redundant Recursive Calls'' . . . . . . 680--685
Keith Clark and
Steve Gregory Parlog: parallel programming in logic 1--49
George B. Leeman, Jr. A Formal Approach to Undo Operations in
Programming Languages . . . . . . . . . 50--87
Robert M. Keller and
M. Ronan Sleep Applicative Caching . . . . . . . . . . 88--108
Keshav Pingali and
Arvind Efficient Demand-Driven Evaluation. Part
2 . . . . . . . . . . . . . . . . . . . 109--139
Keshav Pingali and
Arvind Clarification of ``Feeding Inputs on
Demand'' in Efficient Demand-Driven
Evaluation. Part 1 . . . . . . . . . . . 140--141
Jayadev Misra Axioms for Memory Access in Asynchronous
Hardware Systems . . . . . . . . . . . . 142--153
Mohamed G. Gouda and
Chung-Kou Chang Proving Liveness for Networks of
Communicating Finite State Machines . . 154--182
Laurian M. Chirica and
David F. Martin Toward Compiler Implementation
Correctness Proofs . . . . . . . . . . . 185--214
C. R. Spooner The ML Approach to the Readable
All-Purpose Language . . . . . . . . . . 215--243
E. M. Clarke and
E. A. Emerson and
A. P. Sistla Automatic Verification of Finite-State
Concurrent Systems Using Temporal Logic
Specifications . . . . . . . . . . . . . 244--263
Thomas J. Sager A Short Proof of a Conjecture of DeRemer
and Pennello . . . . . . . . . . . . . . 264--271
Walter F. Tichy Smart Recompilation . . . . . . . . . . 273--291
Valentin F. Turchin The Concept of a Supercompiler . . . . . 292--325
K. M. Chandy and
Jayadev Misra An Example of Stepwise Refinement of
Distributed Programs: Quiescence
Detection . . . . . . . . . . . . . . . 326--343
Matthew Hennessy Proving Systolic Systems Correct . . . . 344--387
Krzysztof R. Apt Correctness Proofs of Distributed
Termination Algorithms . . . . . . . . . 388--405
Flemming Nielson and
Hanne Riis Nielson Technical Correspondence: Comments on
Georgeff's ``Transformations and
Reduction Strategies for Typed Lambda
Expressions'' . . . . . . . . . . . . . 406--407
F. T. Krogh ACM Algorithms Policy . . . . . . . . . 408--411
Anonymous Information for Authors . . . . . . . . 412--415
Thomas Reps Guest Editor's Introduction . . . . . . 417--418
Daniel Swinehart and
Polle Zellweger and
Richard Beach and
Robert Hagemann A Structural View of the Cedar
Programming Environment . . . . . . . . 419--490
Keith D. Cooper and
Ken Kennedy and
Linda Torczon The impact of interprocedural analysis
and optimizations in the R(n)
programming environment . . . . . . . . 491--523
Mark Moriconi and
Dwight Hare The PegaSys System: Pictures as Formal
Documentation of Large Programs . . . . 524--546
Rolf Bahlke and
Gregor Snelting The PSG System: From Formal Language
Definitions to Interactive Programming
Environments . . . . . . . . . . . . . . 547--576
Susan Horwitz and
Tim Teitelbaum Generating Editing Environments Based on
Relations and Attributes . . . . . . . . 577--608
Anonymous 1986 Author Index . . . . . . . . . . . 609--610
Jeannette M. Wing Writing Larch Interface Language
Specifications . . . . . . . . . . . . . 1--24
Scott D. Carson and
Paul F. Reynolds, Jr. The Geometry of Semaphore Programs . . . 25--53
Manfred Broy and
Martin Wirsing and
Peter Pepper On the Algebraic Definition of
Programming Languages . . . . . . . . . 54--99
Stefan Soko\lowski Soundness of Hoare's Logic: An Automated
Proof Using LCF . . . . . . . . . . . . 100--120
Jacques Cohen and
Timothy J. Hickey Parsing and Compiling Using Prolog . . . 125--163
Michael G. Burke and
Gerald A. Fisher A Practical Method for LR and LL
Syntactic Error Diagnosis and Recovery 164--197
Martin S. Feather Language Support for the Specification
and Development of Composite Systems . . 198--234
Raphael Finkel and
Udi Manber DIB --- a distributed implementation of
backtracking . . . . . . . . . . . . . . 235--256
Robert A. Mueller and
Joseph Varghese Retargetable Microcode Synthesis . . . . 257--276
Christopher W. Fraser and
Eugene W. Myers An Editor for Revision Control . . . . . 277--295
David Alex Lamb IDL: Sharing Intermediate
Representations . . . . . . . . . . . . 297--318
Jeanne Ferrante and
Karl J. Ottenstein and
Joe D. Warren The Program Dependence Graph and its Use
in Optimization . . . . . . . . . . . . 319--349
Arthur Charlesworth The Multiway Rendezvous . . . . . . . . 350--366
Richard C. Holt Data Descriptors: a Compile-Time Model
of Data and Addressing . . . . . . . . . 367--389
Shaula Yemini and
Daniel M. Berry An Axiomatic Treatment of Exception
Handling in an Expression-Oriented
Language . . . . . . . . . . . . . . . . 390--407
Thomas Reps and
Alan Demers Sublinear-Space Evaluation Algorithms
for Attribute Grammars . . . . . . . . . 408--440
Debasish Banerjee A Methodology for Synthesis of Recursive
Functional Programs . . . . . . . . . . 441--462
F. T. Krogh ACM Algorithms Policy . . . . . . . . . 463--466
Anonymous Information for Authors . . . . . . . . 467--470
Michael Sonnenschein Graph Translation Schemes to Generate
Compiler Parts . . . . . . . . . . . . . 473--490
Randy Allen and
Ken Kennedy Automatic Translation of Fortran
Programs to Vector Form . . . . . . . . 491--542
D. J. Rosenkrantz and
H. B. Hunt Efficient Algorithms for Automatic
Construction and Compactification of
Parsing Grammars . . . . . . . . . . . . 543--566
Ed Anson A Generalized Iterative Construct and
Its Semantics . . . . . . . . . . . . . 567--581
Christopher T. Haynes and
Daniel P. Friedman Embedding Continuations in Procedural
Objects . . . . . . . . . . . . . . . . 582--598
Janice E. Cuny and
Lawrence Snyder Conversion from Data-Driven to
Synchronous Execution in Loop Programs 599--617
Lubomir Bic and
Craig Lee A Data-Driven Model for a Subset of
Logic Programming . . . . . . . . . . . 618--645
Jacques Loeckx Algorithmic Specifications: a
Constructive Specification Method for
Abstract Data Types . . . . . . . . . . 646--685
Barbara G. Ryder and
Marvin C. Paull Incremental Data-flow Analysis
Algorithms . . . . . . . . . . . . . . . 1--50
Gregory R. Andrews and
Ronald A. Olsson and
Michael Coffin and
Irving Elshoff and
Kelvin Nilsen and
Titus Purdin and
Gregg Townsend An Overview of the SR Language and
Implementation . . . . . . . . . . . . . 51--86
W. H. Hesselink A Mathematical Approach to
Nondeterminism in Data Types . . . . . . 87--117
Raymond T. Boute System Semantics: Principles,
Applications, and Implementation . . . . 118--155
Joylyn Reed and
Raymond T. Yeh Specification and Verification of
Liveness Properties of Cyclic,
Concurrent Processes . . . . . . . . . . 156--177
Sandra L. Murphy and
A. Udaya Shankar A Note on the Drinking Philosophers
Problem (Technical Correspondence) . . . 178--188
Paul N. Hilfinger An Ada Package for Dimensional Analysis 189--203
Niklaus Wirth Type Extensions . . . . . . . . . . . . 204--214
Jan van den Bos Abstract Interaction Tools: a Language
for User Interface Management Systems 215--247
Daniel Le Métayer ACE: An Automatic Complexity Evaluator 248--266
Leslie Lamport Control Predicates are Better than Dummy
Variables for Reasoning about Program
Control . . . . . . . . . . . . . . . . 267--281
Dennis Shasha and
Marc Snir Efficient and Correct Execution of
Parallel Programs that Share Memory . . 282--312
Albert G. Greenberg and
Boris D. Lubachevsky and
Andrew M. Odlyzko Simple, Efficient, Asynchronous Parallel
Algorithms for Maximization . . . . . . 313--337
Manuel E. Bermudez and
Karl M. Schimpf On the (non-) Relationship between
SLR(1) and NQLALR(1) Grammars (Technical
Correspondence) . . . . . . . . . . . . 338--342
Pierpaolo Degano and
Stefano Mannucci and
Bruno Mojana Efficient Incremental LR Parsing for
Syntax-Directed Editors . . . . . . . . 345--373
Laura K. Dillon and
George S. Avrunin and
Jack C. Wiledon Constrained Expressions: Toward Broad
Applicability of Analysis Methods for
Distributed Software Systems . . . . . . 374--402
Carroll Morgan The Specification Statement . . . . . . 403--419
Ernst-Rüdiger Olderog and
Krzysztof R. Apt Fairness in Parallel Programs: The
Transformational Approach . . . . . . . 420--455
Jon Mauney and
Charles N. Fischer Determining the Extent of Lookahead in
Syntactic Error Repair . . . . . . . . . 456--469
John C. Mitchell and
Gordon D. Plotkin Abstract Types Have Existential Type . . 470--502
Shaula Yemini and
Daniel M. Berry Technical Correspondence: ``An Axiomatic
Treatment of Exception Handling in an
Expression-Oriented Language'' . . . . . 503--504
F. T. Krogh ACM Algorithms Policy . . . . . . . . . 504--507
Anonymous Information for Authors . . . . . . . . 508--511
R. J. R. Back and
R. Kurki-Suonio Distributed Cooperation with Action
Systems . . . . . . . . . . . . . . . . 513--554
Katsuro Inoue and
Hiroyuki Seki and
Hikaru Yagi Analysis of Functional Programs to
Detect Run-Time Garbage Cells . . . . . 555--578
Clyde P. Kruskal and
Larry Rudolph and
Marc Snir Efficient Synchronization on
Multiprocessors with Shared Memory . . . 579--601
Richard Kennaway and
Ronan Sleep Director Strings as Combinators . . . . 602--626
Robert W. Schwanke and
Gail E. Kaiser Smarter Recompilation . . . . . . . . . 627--632
Walter F. Tichy Technical Correspondence: Tichy's
Response to R. W. Schwanke and G. E.
Kaiser's ``Smarter Recompilation'' . . . 633--634
Karl-Heinz Drechsler and
Manfred P. Stadel Technical Correspondence: a Solution to
a Problem with Morel and Renvoise's
``Global Optimization by Suppression of
Partial Redundancies'' . . . . . . . . . 635--640
Anonymous 1988 Author Index . . . . . . . . . . . 641--642
Peter A. Steenkiste and
John L. Hennessy A Simple Interprocedural Register
Allocation Algorithm and Its
Effectiveness for Lisp . . . . . . . . . 1--32
Eugene W. Myers and
Webb Miller Row Replacement Algorithms for Screen
Editors . . . . . . . . . . . . . . . . 33--56
David Bernstein and
Izidor Gertner Scheduling Expressions on a Pipelined
Processor with a Maximal Delay of One
Cycle . . . . . . . . . . . . . . . . . 57--66
J. Steensgaard-Madsen Type Representation of Objects by
Functions . . . . . . . . . . . . . . . 67--89
Michael J. Fischer and
Nancy A. Lynch and
James E. Burns and
Allan Borodin Distributed FIFO Allocation of Identical
Resources Using Small Shared Space . . . 90--114
Hassan A\"\it-Kaci and
Robert Boyer and
Patrick Lincoln and
Roger Nasr Efficient Implementation of Lattice
Operations . . . . . . . . . . . . . . . 115--146
Bowen Alpern and
Fred B. Schneider Verifying Temporal Properties without
Temporal Logic . . . . . . . . . . . . . 147--167
Gail E. Kaiser Incremental Dynamic Semantics for
Language-Based Programming Environments 169--193
Robert D. Cameron Efficient High-Level Iteration with
Accumulators . . . . . . . . . . . . . . 194--211
Wilf R. LaLonde Designing Families of Data Types Using
Exemplars . . . . . . . . . . . . . . . 212--248
William E. Weihl Local Atomicity Properties: Modular
Concurrency Control for Abstract Data
Types . . . . . . . . . . . . . . . . . 249--283
Vincenza Carchiolo and
Antonella Di Stefano and
Alberto Faro and
Giuseppe Pappalardo ECCS and LIPS: Two Languages for OSI
Systems Specification and Verification 284--329
James E. Burns and
Jan Pachi Uniform Self-Stabilizing Rings . . . . . 330--344
Susan Horwitz and
Jan Prins and
Thomas Reps Integrating Noninterfering Versions of
Programs . . . . . . . . . . . . . . . . 345--387
R. P. Brent Efficient Implementation of the
First-Fit Strategy for Dynamic Storage
Allocation . . . . . . . . . . . . . . . 388--403
Frank D. Anger On Lamport's Interprocessor
Communication Model . . . . . . . . . . 404--417
Saumya K. Debray Static Inference of Modes and Data
Dependencies in Logic Programs . . . . . 418--450
Saumya K. Debray and
David S. Warren Functional Computations in Logic
Programs . . . . . . . . . . . . . . . . 451--481
Richard Kennaway and
Ronan Sleep Corrigendum: ``Director Strings as
Combinators'' . . . . . . . . . . . . . 482--482
F. T. Krogh ACM Algorithms Policy . . . . . . . . . 483--486
Anonymous Information for Authors . . . . . . . . 487--490
Alfred V. Aho and
Mahadevan Ganapathi and
Steven W. K. Tjiang Code Generation Using Tree Matching and
Dynamic Programming . . . . . . . . . . 491--516
Greg Nelson A Generalization of Dijkstra's Calculus 517--561
Valmir Barbosa and
Eli Gafni Concurrency in Heavily Loaded
Neighborhood-Constrained Systems . . . . 562--584
Rajive Bagrodia Synchronization of Asynchronous
Processes in CSP . . . . . . . . . . . . 585--597
Arvind and
Rishiyur S. Nikhil and
Keshav K. Pingali I-Structures: Data Structures for
Parallel Computing . . . . . . . . . . . 598--632
Ben A. Sijtsma On the Productivity of Recursive List
Definitions . . . . . . . . . . . . . . 633--649
Tim Nicholson and
Norman Foo A Denotational Semantics for Prolog . . 650--665
Arthur Sorkin Technical Correspondence: Some Comments
on ``A Solution to a Problem with Morel
and Renvoise's ``Global Optimization by
Suppression of Partial Redundancies'''' 666--668
Anonymous 1989 Author Index . . . . . . . . . . . 669--670
Geoffrey Clemm and
Leon Osterweil A Mechanism for Environment Integration 1--25
Susan Horwitz and
Thomas Reps and
David Binkley Interprocedural Slicing Using Dependence
Graphs . . . . . . . . . . . . . . . . . 26--60
Vance E. Waddle Production Trees: a Compact
Representation of Parsed Programs . . . 61--83
E. Korach and
S. Kutten and
S. Moran A Modular Technique for the Design of
Efficient Distributed Leader Finding
Algorithms . . . . . . . . . . . . . . . 84--101
Shing-Tsaan Huang A Distributed Deadlock Detection
Algorithm for CSP-Like Communication . . 102--122
William M. Farmer and
John D. Ramsdell and
Ronald J. Watro A Correctness Proof for Combinator
Reduction with Cycles . . . . . . . . . 123--134
F. Warren Burton Technical Correspondence: Type Extension
Through Polymorphism . . . . . . . . . . 135--138
David L. Parnas Technical Correspondence: On Iterative
Constructs . . . . . . . . . . . . . . . 139--141
Brad A. Myers Creating User Interfaces Using
Programming by Example, Visual
Programming, and Constraints . . . . . . 143--177
William E. Weihl Linguistic Support for Atomic Data Types 178--202
Edgar Knapp An Exercise in the Formal Derivation of
Parallel Programs: Maximum Flows in
Graphs . . . . . . . . . . . . . . . . . 203--223
Jared L. Darlington Search Direction by Goal Failure in
Goal-Oriented Programming . . . . . . . 224--252
A. Bossi and
N. Cocco and
S. Dulli A Method for Specializing Logic Programs 253--302
S. Aggarwal and
C. Courcoubetis and
P. Wolper Adding Liveness Properties to Coupled
Finite-State Machines . . . . . . . . . 303--339
Michael Burke An Interval-Based Approach to Exhaustive
and Incremental Interprocedural
Data-Flow Analysis . . . . . . . . . . . 341--395
Leslie Lamport \sl win and \sl sin: Predicate
Transformers for Concurrency . . . . . . 396--428
Larry G. Jones Efficient Evaluation of Circular
Attribute Grammars . . . . . . . . . . . 429--462
Maurice P. Herlihy and
Jeannette M. Wing Linearizability: a Correctness Condition
for Concurrent Objects . . . . . . . . . 463--492
F. T. Krogh ACM Algorithms Policy . . . . . . . . . 493--496
Anonymous Information for Authors . . . . . . . . 497--500
Fred C. Chow and
John L. Hennessy The Priority-Based Coloring Approach to
Register Allocation . . . . . . . . . . 501--536
James W. Stamos and
David K. Gifford Remote Evaluation . . . . . . . . . . . 537--565
Prasun Dewan and
Marvin Solomon An Approach to Support Automatic
Generation of User Interfaces . . . . . 566--609
Hans Leiss On Kilbury's Modification of Earley's
Algorithm . . . . . . . . . . . . . . . 610--640
Dewayne E. Perry Guest Editor's Introduction . . . . . . 641--642
Laura K. Dillon Using Symbolic Execution for
Verification of Ada Tasking Programs . . 643--669
Jack C. Wileden and
Lori A. Clarke and
Alexander L. Wolf A Comparative Evaluation of Object
Definition Techniques for Large
Prototype Systems . . . . . . . . . . . 670--699
Anonymous 1990 Author Index . . . . . . . . . . . 700--701
Russell W. Quong and
Mark A. Linton Linking Programs Incrementally . . . . . 1--20
Pascal Fradet and
Daniel Le Métayer Compilation of Functional Languages by
Program Transformation . . . . . . . . . 21--51
Richard C. Waters Automatic Transformation of Series
Expressions into Loops . . . . . . . . . 52--98
Antonio Brogi and
Paolo Ciancarini The Concurrent Language, Shared Prolog 99--123
Maurice Herlihy Wait-Free Synchronization . . . . . . . 124--149
M. Ancona and
G. Dodero and
V. Gianuzzi and
M. Morgavi Efficient Construction of LR$ (k) $
States and Tables . . . . . . . . . . . 150--178
Jack C. Wileden and
Lori A. Clarke and
Alexander L. Wolf Corrigenda: ``A Comparative Evaluation
of Object Definition Techniques for
Large Prototype Systems'' . . . . . . . 179--179
Mark N. Wegman and
F. Kenneth Zadeck Constant Propagation with Conditional
Branches . . . . . . . . . . . . . . . . 181--210
Daniel M. Yellin and
Robert E. Strom INC: a Language for Incremental
Computations . . . . . . . . . . . . . . 211--236
Martín Abadi and
Luca Cardelli and
Benjamin Pierce and
Gordon Plotkin Dynamic Typing in a Statically Typed
Language . . . . . . . . . . . . . . . . 237--268
Paul Hudak and
Jonathan Young Collecting Interpretations of
Expressions . . . . . . . . . . . . . . 269--290
Dhananjay M. Dhamdhere Practical Adaptation of the Global
Optimization Algorithm of Morel and
Renvoise . . . . . . . . . . . . . . . . 291--294
Jürgen Börstler and
Ulrich Möncke and
Reinhard Wilhelm Table Compression for Tree Automata . . 295--314
Scott E. Hudson Incremental Attribute Evaluation: a
Flexible Algorithm for Lazy Update . . . 315--341
R. Morrison and
A. Dearle and
R. C. H. Connor and
A. L. Brown An Ad Hoc Approach to the Implementation
of Polymorphism . . . . . . . . . . . . 342--371
Thomas P. Murtagh An Improved Storage Management Scheme
for Block Structured Languages . . . . . 372--398
Wuxu Peng and
S. Purushothaman Data Flow Analysis of Communicating
Finite State Machines . . . . . . . . . 399--442
Fred T. Krogh ACM Algorithms Policy . . . . . . . . . 443--446
Anonymous Information for Authors . . . . . . . . 447--450
Ron Cytron and
Jeanne Ferrante and
Barry K. Rosen and
Mark N. Wegman and
F. Kenneth Zadeck Efficiently Computing Static Single
Assignment Form and the Control
Dependence Graph . . . . . . . . . . . . 451--490
Jong-Deok Choi and
Barton P. Miller and
Robert H. B. Netzer Techniques for Debugging Parallel
Programs with Flowback Analysis . . . . 491--530
Tim Sheard Automatic Generation and Use of Abstract
Structure Operators . . . . . . . . . . 531--557
Edward A. Lycklama and
Vassos Hadzilacos A First-Come-First-Served
Mutual-Exclusion Algorithm with Small
Communication Variables . . . . . . . . 558--576
Radha Jagadeesan and
Keshav Pingali and
Prakash Panangaden A Fully Abstract Semantics for a
First-Order Functional Language with
Logic Variables . . . . . . . . . . . . 577--625
Norman H. Cohen Technical Correspondence: Type-Extension
Type Tests Can Be Performed In Constant
Time . . . . . . . . . . . . . . . . . . 626--629
Niklaus Wirth Technical Correspondence: Reply to
``Type-Extension Tests Can Be Performed
In Constant Time'' . . . . . . . . . . . 630--630
Dennis M. Volpano Technical Correspondence: Subtypes and
Quantification . . . . . . . . . . . . . 631--632
F. Warren Burton Technical Correspondence: Author's Reply
to ``Subtypes and Quantification'', by
D. M. Volpano . . . . . . . . . . . . . 633--633
S. Purushothaman Corrigendum: ``Data Flow Analysis of
Communicating Finite State Machines'' 633--633
Anonymous 1991 Author Index . . . . . . . . . . . 634--635
David Ungar and
Frank Jackson An Adaptive Tenuring Policy for
Generation Scavengers . . . . . . . . . 1--27
Jon A. Solworth Epochs . . . . . . . . . . . . . . . . . 28--53
Timothy J. Hickey and
Jacques Cohen and
Hitofumi Hotta and
Thierry PetitJean Computer-Assisted Microanalysis of
Parallel Programs . . . . . . . . . . . 54--106
David A. Gudeman Denotational Semantics of a
Goal-Directed Language . . . . . . . . . 107--125
Raymond T. Boute The Euclidean Definition of the
Functions div and mod . . . . . . . . . 127--144
Alexander L. Wolf Guest Editor's Introduction to the
Special Section on the Third
International Conference on Computer
Languages . . . . . . . . . . . . . . . 145--146
Carsten K. Gomard A Self-applicable Partial Evaluator for
the Lambda Calculus: Correctness and
Pragmatics . . . . . . . . . . . . . . . 147--172
Lori L. Pollock and
Mary Lou Soffa Incremental Global Reoptimization of
Programs . . . . . . . . . . . . . . . . 173--200
Gail E. Kaiser and
Brent Hailpern An Object-Based Programming Model for
Shared Data . . . . . . . . . . . . . . 201--264
Philip J. Koopman, Jr. and
Peter Lee and
Daniel P. Siewiorek Cache Behavior of Combinator Graph
Reduction . . . . . . . . . . . . . . . 265--297
David W. Wall Experience with a Software-Defined
Machine Architecture . . . . . . . . . . 299--338
Joxan Jaffar and
Spiro Michaylov and
Peter J. Stuckey and
Roland H. C. Yap The CLP($ \cal R$) Language and System 339--395
Jennifer Widom and
David Gries and
F. B. Schneider Trace-Based Network Proof Systems:
Expressiveness and Completeness . . . . 396--416
A. Udaya Shankar and
Simon S. Lam A Stepwise Refinement Heuristic for
Protocol Construction . . . . . . . . . 417--461
Fred T. Krogh ACM Algorithms Policy . . . . . . . . . 462--465
Anonymous Information for Authors . . . . . . . . 466--469
Wilfred J. Hansen Subsequence References: First-Class
Values for Substrings . . . . . . . . . 471--489
J. Heering and
P. Klint and
J. Rekers Incremental Generation of Lexical
Scanners . . . . . . . . . . . . . . . . 490--520
Angelo Morzenti and
Dino Mandrioli and
Carlo Ghezzi A Model Parametric Real-Time Logic . . . 521--573
Jacob Katzenelson and
Shlomit S. Pinter and
Eugen Schenfeld Type Matching, Type-Graphs, and the
Schanuel Conjecture . . . . . . . . . . 574--588
Robert Muller M-LISP: a Representation-Independent
Dialect of LISP with Reduction Semantics 589--616
Anonymous 1992 Author Index . . . . . . . . . . . 617--618
Gerard Tel and
Friedmann Mattern The Derivation of Distributed
Termination Detection Algorithms from
Garbage Collection Schemes . . . . . . . 1--35
Rance Cleaveland and
Joachim Parrow and
Bernhard Steffen The Concurrency Workbench: a
Semantics-Based Tool for the
Verification of Concurrent Systems . . . 36--72
Martín Abadi and
Leslie Lamport Composing Specifications . . . . . . . . 73--132
Roberto Barbuti and
Roberto Giacobazzi and
Giorgio Levi A General Framework for Semantics-Based
Bottom-Up Abstract Interpretation of
Logic Programs . . . . . . . . . . . . . 133--181
Yehuda Afek and
Geoffrey Brown and
Michael Merritt Lazy Caching . . . . . . . . . . . . . . 182--205
Alan Finlay and
Lloyd Allison Technical Correspondence: a Correction
to the Denotational Semantics for the
Prolog of Nicholson and Foo . . . . . . 206--208
Jennifer Widom and
David Gries and
F. B. Schneider Corrigendum: ``Trace-Based Network Proof
Systems: Expressiveness and
Completeness'' . . . . . . . . . . . . . 208--208
Andrew W. Appel Editorial . . . . . . . . . . . . . . . 209--210
Robert Harper and
John C. Mitchell On the Type Structure of Standard ML . . 211--252
Fritz Henglein Type Inference with Polymorphic
Recursion . . . . . . . . . . . . . . . 253--289
A. J. Kfoury and
J. Tiuryn and
P. Urzyczyn Type Recursion in the Presence of
Polymorphic Recursion . . . . . . . . . 290--311
Dhananjay M. Dhamdhere and
Harish Patil An Elimination Algorithm for
Bidirectional Data Flow Problems Using
Edge Placement . . . . . . . . . . . . . 312--336
Shmuel Katz A Superimposition Control Construct for
Distributed Systems . . . . . . . . . . 337--356
Max Copperman and
Charles E. McDowell Technical Correspondence: a Further Note
on Hennessy's ``Symbolic Debugging of
Optimized Code'' . . . . . . . . . . . . 357--365
Michael Burke and
Linda Torczon Interprocedural Optimization:
Eliminating Unnecessary Recompilation 367--399
Siddhartha Chatterjee Compiling Nested Data-Parallel Programs
for Shared-Memory Multiprocessors . . . 400--462
Charles Consel and
Siau Cheng Khoo Parameterized Partial Evaluation . . . . 463--493
Joel E. Richardson and
Michael J. Carey and
Daniel T. Schuh The Design of the E Programming Language 494--534
Martin Odersky Defining Context-Dependent Syntax
Without Using Contexts . . . . . . . . . 535--562
Shing-Tsaan Huang Leader Election in Uniform Rings . . . . 563--573
Roberto M. Amadio and
Luca Cardelli Subtyping Recursive Types . . . . . . . 575--631
Krishna V. Palem and
Barbara B. Simons Scheduling Time-Critical Instructions on
RISC Machines . . . . . . . . . . . . . 632--658
Gopal Gupta and
Bharat Jayaraman Analysis of Or-Parallel Execution Models 659--680
C. J. Fidge A Formal Definition of Priority in CSP 681--705
Martín Abadi and
Michael Burrows and
Butler Lampson and
Gordon Plotkin A Calculus for Access Control in
Distributed Systems . . . . . . . . . . 706--734
Sukumar Ghosh An Alternative Solution to a Problem on
Self-Stabilization . . . . . . . . . . . 735--742
A. W. Appel and
S. L. Graham Editorial . . . . . . . . . . . . . . . 743--744
Maurice Herlihy A Methodology for Implementing Highly
Concurrent Data Objects . . . . . . . . 745--770
Jonathan I. Leivent and
Ronald J. Watro Mathematical Foundations for Time Warp
Systems . . . . . . . . . . . . . . . . 771--794
Mic Bowman and
Saumya K. Debray and
Larry L. Peterson Reasoning About Naming Systems . . . . . 795--825
Saumya K. Debray and
Nai-Wei Lin Cost Analysis of Logic Programs . . . . 826--875
Huimin Lin Procedural Implementation of Algebraic
Specification . . . . . . . . . . . . . 876--895
Andrew Appel Purpose and Scope . . . . . . . . . . . 1--2
E. Tick and
M. Korsloot Determinacy Testing for Nondeterminate
Logic Programming Languages . . . . . . 3--34
Baudouin Le Charlier and
Pascal Van Hentenryck Experimental Evaluation of a Generic
Abstract Interpretation Algorithm for
PROLOG . . . . . . . . . . . . . . . . . 35--101
Richard C. Waters Cliché-Based Program Editors . . . . . . 102--150
James M. Purtilo The POLYLITH Software Bus . . . . . . . 151--174
Mary Jean Harrold and
Mary Lou Soffa Efficient Computation of Interprocedural
Definition-Use Chains . . . . . . . . . 175--204
Anne Mulkers and
William Winsborough and
Maurice Bruynooghe Live-Structure Dataflow Analysis for
Prolog . . . . . . . . . . . . . . . . . 205--258
Bengt Jonsson Compositional Specification and
Verification of Distributed Systems . . 259--303
Shlomit S. Pinter and
Ron Y. Pinter Program Optimization and Parallelization
Using Idioms . . . . . . . . . . . . . . 305--327
Adrienne Bloss Path Analysis and the Optimization of
Nonstrict Functional Languages . . . . . 328--369
Rajiv Gupta and
Mary Lou Soffa and
Denise Ombres Efficient Register Allocation via
Coloring Using Clique Separators . . . . 370--386
Max Copperman Debugging Optimized Code Without Being
Misled . . . . . . . . . . . . . . . . . 387--427
Preston Briggs and
Keith D. Cooper and
Linda Torczon Improvements to Graph Coloring Register
Allocation . . . . . . . . . . . . . . . 428--455
Suresh Jagannathan Metalevel Building Blocks for Modular
Systems . . . . . . . . . . . . . . . . 456--492
J. R. Kennaway and
J. W. Klop and
M. R. Sleep and
F. J. De Vries On the Adequacy of Graph Rewriting for
Simulating Term Rewriting . . . . . . . 493--523
Lawrence A. Crowl and
Thomas J. LeBlanc Parallel Programming with Control
Abstraction . . . . . . . . . . . . . . 524--576
Ian Foster and
Stephen Taylor A Compiler Approach to Scalable
Concurrent-Program Design . . . . . . . 577--604
Bijan Arbab and
Daniel Berry Some Comments on ``A Denotational
Semantics for Prolog'' . . . . . . . . . 605--606
Kim Marriott and
Harald Sòndergaard and
Neil D. Jones Denotational Abstract Interpretation of
Logic Programs . . . . . . . . . . . . . 607--648
Michael Codish and
Moreno Falaschi and
Kim Marriott Suspension Analyses for Concurrent Logic
Programs . . . . . . . . . . . . . . . . 649--686
Krzysztof R. Apt and
Alessando Pellegrini On the Occur-Check-Free Prolog Programs 687--726
David Garlan and
Charles W. Krueger and
Barbara S. Lerner TransformGen: Automating the Maintenance
of Structure-Oriented Environments . . . 727--774
Lin Yu and
Daniel J. Rosenkrantz A Linear-Time Scheme for Version
Reconstruction . . . . . . . . . . . . . 775--797
Josyula R. Rao Reasoning about Probabilistic Parallel
Programs . . . . . . . . . . . . . . . . 798--842
Orna Grumberg and
David E. Long Model Checking and Modular Verification 843--871
Leslie Lamport The Temporal Logic of Actions . . . . . 872--923
Manfred Broy and
Greg Nelson Adding Fair Choice to Dijkstra's
Calculus . . . . . . . . . . . . . . . . 924--938
Yehuda Afek and
Danny Dolev and
Eli Gafni and
Michael Merritt and
Nir Shavit A Bounded First-In, First-Enabled
Solution to the $ \ell $-Exclusion
Problem . . . . . . . . . . . . . . . . 939--953
Yuh-Jzer Joung and
Scott A. Smolka Coordinating First-Order Multiparty
Interactions . . . . . . . . . . . . . . 954--985
Michael K. Reiter and
Kenneth P. Birman How to Securely Replicate Services . . . 986--1009
J. Heering and
P. Klint and
J. Rekers Lazy and Incremental Program Generation 1010--1023
Mikkel Thorup Controlled Grammatic Ambiguity . . . . . 1024--1050
Joseph Bates and
Alon Lavie Recognizing Substrings of LR$ (k) $
Languages in Linear Time . . . . . . . . 1051--1077
Andrew Appel and
Charles Fischer Editorial . . . . . . . . . . . . . . . 1079--1079
Annalisa Bossi and
Sandro Etalle Transforming Acyclic Programs . . . . . 1081--1096
Jong-Deok Choi and
Jeanne Ferrante Static Slicing in the Presence of Goto
Statements . . . . . . . . . . . . . . . 1097--1113
Michael Wolfe The Definition of Dependence Distance 1114--1116
Jens Knoop and
Oliver Rüthing and
Bernhard Steffen Optimal Code Motion: Theory and Practice 1117--1155
Stefan Freudenberger and
Thomas R. Gross and
P. Geoffrey Lowney Avoidance and Suppression of
Compensation Code in a Trace Scheduling
Compiler . . . . . . . . . . . . . . . . 1156--1214
John Hannan Operational Semantics-Directed Compilers
and Machine Architectures . . . . . . . 1215--1247
William Pugh and
David Wonnacott Static Analysis of Upper and Lower
Bounds on Dependences and Parallelism 1248--1278
Hassan A\"\it-Kaci and
Andreas Podelski Functions as Passive Constraints in LIFE 1279--1318
Thomas Ball and
James R. Larus Optimally Profiling and Tracing Programs 1319--1360
Antonio Brogi and
Paolo Mancarella and
Dino Pedreschi and
Franco Turini Modular Logic Programming . . . . . . . 1361--1398
Thomas Ball Efficiently Counting Program Events with
Support for On-Line Queries . . . . . . 1399--1410
Konstantin Läufer and
Martin Odersky Polymorphic Type Inference and Abstract
Data Types . . . . . . . . . . . . . . . 1411--1430
J. Michael Ashley and
Charles Consel Fixpoint Computation for Polyvariant
Static Analyses of Higher-Order
Applicative Programs . . . . . . . . . . 1431--1448
Marcel Beemster Strictness Optimization for Graph
Reduction Machines (Why id Might Not Be
Strict) . . . . . . . . . . . . . . . . 1449--1466
G. Ramalingam The Undecidability of Aliasing . . . . . 1467--1471
Uday P. Khedker and
Dhananjay M. Dhamdhere A Generalized Theory of Bit Vector Data
Flow Analysis . . . . . . . . . . . . . 1472--1511
Edmund M. Clarke and
Orna Grumberg and
David E. Long Model Checking and Abstraction . . . . . 1512--1542
Martín Abadi and
Leslie Lamport An Old-Fashioned Recipe for Real Time 1543--1571
Josephine Micallef and
Gail E. Kaiser Extending Attribute Grammers to Support
Programming-in-the-Large . . . . . . . . 1572--1612
Peter T. Breuer and
Jonathan P. Bowen Decompilation: The Enumeration of Types
and Grammers . . . . . . . . . . . . . . 1613--1647
David B. Whalley Automatic Isolation of Compiler Errors 1648--1659
J. J. \vZic Time-Constrained Buffer Specifications
in CSP+T and Timed CSP . . . . . . . . . 1661--1674
A. P. W. Böhm and
R. R. Oldehoeft Two Issues in Parallel Language Design 1675--1683
M. M. Brandis and
H. Moessenboeck Single-Pass Generation of Static
Single-Assignment Form for Structured
Languages . . . . . . . . . . . . . . . 1684--1698
A. W. Appel Axiomatic Bootstrapping: a Guide for
Compiler Hackers . . . . . . . . . . . . 1699--1718
N. Haines and
D. Kindred and
J. G. Morrisett and
S. M. Nettles Composing First-Class Transactions . . . 1719--1736
J. Misra Powerlist: a Structure for Parallel
Recursion . . . . . . . . . . . . . . . 1737--1767
S. Carr and
K. Kennedy Improving the Ratio of Memory Operations
in Floating-Point Operations in Loops 1768--1810
B. H. Liskov and
J. M. Wing A Behavioral Notion of Subtyping . . . . 1811--1841
D. G. Von Bank and
C. M. Shub and
R. W. Sebesta A Unified Model of Pointwise Equivalence
of Procedural Computations . . . . . . . 1842--1874
V. Berzins Software Merge: Semantics of Combining
Changes to Programs . . . . . . . . . . 1875--1903
Anonymous 1994 Author Index . . . . . . . . . . . 1904--1907
J.-M. Larchevêque Optimal Incremental Parsing . . . . . . 1--15
Yih-Kuen Tsay and
Rajive L. Bagrodia Deducing Fairness Properties in UNITY
Logic --- a New Completeness Result . . 16--27
Michael Codish and
Anne Mulkers and
Maurice Bruynooghe and
Maria Garcia de la Banda and
Manuel Hermenegildo Improving Abstract Interpretations by
Combining Domains . . . . . . . . . . . 28--44
Joseph P. Skudlarek Notes on ``A Methodology for
Implementing Highly Concurrent Data
Objects'' . . . . . . . . . . . . . . . 45--46
Jens Palsberg Closure Analysis in Constraint Form . . 47--62
Alexander Aiken and
John H. Williams and
Edward L. Wimmers Safe: a Semantic Technique for
Transforming Programs in the Presence of
Errors . . . . . . . . . . . . . . . . . 63--84
Michael P. Gerlek and
Eric Stoltz and
Michael Wolfe Beyond Induction Variables: Detecting
and Classifying Sequences Using a
Demand-Driven SSA Form . . . . . . . . . 85--122
Siddhartha Chatterjee and
John R. Gilbert and
Robert Schreiber and
Shang-Hua Teng Optimal Evaluation of Array Expressions
on Massively Parallel Machines . . . . . 123--156
Bernadette Charron-Bost and
Carole Delporte-Gallet and
Hugues Fauconnier Local and Temporal Predicates in
Distributed Systems . . . . . . . . . . 157--179
Xiaolei Qian and
Allen Goldberg Corrigendum: ``Referential Opacity in
Nondeterministic Data Refinement'' . . . 180--180
Cliff Click and
Keith D. Cooper Combining Analyses, Combining
Optimizations . . . . . . . . . . . . . 181--196
G. A. Venkatesh Experimental Results from Dynamic
Slicing of C Programs . . . . . . . . . 197--216
Wei-Ngan Chin and
Eak-Khoon Goh A Reexamination of ``Optimization of
Array Subscript Range Checks'' . . . . . 217--227
Pei-Chi Wu and
Feng-Jian Wang A Worst Case of Circularity Test
Algorithms for Attribute Grammars . . . 228--232
Anne Rogers and
Martin C. Carlisle and
John H. Reppy and
L. J. Hendren Supporting Dynamic Data Structures on
Distributed-Memory Machines . . . . . . 233--263
Jens Palsberg and
Cun Xiao and
Karl Lieberherr Efficient Implementation of Adaptive
Software . . . . . . . . . . . . . . . . 264--292
Adam Webber Optimization of Functional Programs by
Grammar Thinning . . . . . . . . . . . . 293--330
Saumya K. Debray On the Complexity of Dataflow Analysis
of Logic Programs . . . . . . . . . . . 331--365
Michal Walicki and
Sigurd Meidal A Complete Calculus for the
Multialgebraic and Functional Semantics
of Nondeterminism . . . . . . . . . . . 366--393
Alan Carle and
Lori Pollock Matching-Based Incremental Evaluators
for Hierarchical Attribute Grammar
Dialects . . . . . . . . . . . . . . . . 394--429
Giuseppe Castagna Covariance and Contravariance: Conflict
without a Cause . . . . . . . . . . . . 431--447
W. H. Carlisle Type Checking Concurrent I/O . . . . . . 448--460
Todd A. Proebsting BURS Automata Generation . . . . . . . . 461--486
Ron K. Cytron and
Jeanne Ferrante Efficiently Computing $ \phi $-Nodes
On-The-Fly . . . . . . . . . . . . . . . 487--506
Martin Abadi and
Leslie Lamport Conjoining Specifications . . . . . . . 507--534
Manhoi Choy and
Ambuj K. Singh Efficient Fault-Tolerant Algorithms for
Distributed Resource Allocation . . . . 535--559
Christine Fricker and
Olivier Temam and
William Jalby Influence of Cross-Interferences on
Blocked Loops: a Case Study with
Matrix-Vector Multiply . . . . . . . . . 561--575
Jens Palsberg and
Patrick O'Keefe A Type System Equivalent to Flow
Analysis . . . . . . . . . . . . . . . . 576--599
Milind Girkar and
Constantine D. Polychronopoulos Extracting Task-Level Parallelism . . . 600--634
Pascal Van Hentenryck and
Viswanath Ramachandran Backtracking without Trailing in CLP($
{\cal R}_{\hbox {Lin}}$) . . . . . . . . 635--671
Bruce J. McKenzie and
Corey Yeatman and
Lorraine De Vere Error Repair in Shift-Reduce Parsers . . 672--689
Anthony M. Sloane An Evaluation of an Automatically
Generated Compiler . . . . . . . . . . . 691--703
Henry Cejtin and
Suresh Jagannathan and
Richard Kelsey Higher-Order Distributed Objects . . . . 704--739
Steven M. Kurlander and
Todd A. Proebsting and
Charles N. Fischer Efficient Instruction Scheduling for
Delayed-Load Architectures . . . . . . . 740--776
Stephen P. Masticola and
Thomas J. Marlowe and
Barbara G. Ryder Lattice Frameworks for Multisource and
Bidirectional Data Flow Problems . . . . 777--803
Craig Chambers and
Gary T. Leavens Typechecking and Modules for
Multimethods . . . . . . . . . . . . . . 805--843
Atsushi Ohori A Polymorphic Record Calculus and Its
Compilation . . . . . . . . . . . . . . 844--895
R. Sekar and
I. V. Ramakrishnan Fast Strictness Analysis Based on Demand
Propagation . . . . . . . . . . . . . . 896--937
Anonymous 1995 Author Index . . . . . . . . . . . 938--940
Stephan Murer and
Stephen Omohundro and
David Stoutamire and
Clemens Szyperski Iteration abstraction in Sather . . . . 1--15
Alan Carle and
Lori Pollock On the optimality of change propagation
for incremental evaluation of
hierarchical attribute grammars . . . . 16--29
Brad Vander Zanden An incremental algorithm for satisfying
hierarchies of multiway dataflow
constraints . . . . . . . . . . . . . . 30--72
John Tang Boyland Conditional attribute grammars . . . . . 73--108
Cordelia V. Hall and
Kevin Hammond and
Simon L. Peyton Jones and
Philip L. Wadler Type classes in Haskell . . . . . . . . 109--138
John R. Hauser Handling floating-point exceptions in
numeric programs . . . . . . . . . . . . 139--174
David Sands Total correctness by local improvement
in the transformation of functional
programs . . . . . . . . . . . . . . . . 175--234
Stan Liao and
Srinivas Devadas and
Kurt Keutzer and
Steven Tjiang and
Albert Wang Storage assignment to decrease code size 235--253
Geoffrey Smith and
Dennis Volpano Polymorphic typing of variables and
references . . . . . . . . . . . . . . . 254--267
Jens Knoop and
Bernhard Steffen and
Jürgen Vollmer Parallelism for free: efficient and
optimal bitvector analyses for parallel
programs . . . . . . . . . . . . . . . . 268--299
Lal George and
Andrew W. Appel Iterated register coalescing . . . . . . 300--324
Carroll Morgan and
Annabelle McIver and
Karen Seidel Probabilistic predicate transformers . . 325--353
Brad Vander Zanden Corrigendum: ``An incremental algorithm
for satisfying hierarchies of multiway
dataflow constraints'' . . . . . . . . . 354--354
Urs Hölzle and
David Ungar Reconciling Responsiveness with
Performance in Pure Object-Oriented
Languages . . . . . . . . . . . . . . . 355--400
Martín Abadi and
Luca Cardelli On Subtyping and Matching . . . . . . . 401--423
Kathryn S. McKinley and
Steve Carr and
Chau-Wen Tseng Improving Data Locality with Loop
Transformations . . . . . . . . . . . . 424--453
Ian Foster Compositional Parallel Programming
Languages . . . . . . . . . . . . . . . 454--476
Mohammad R. Haghighat and
Constantine D. Polychronopoulos Symbolic Analysis for Parallelizing
Compilers . . . . . . . . . . . . . . . 477--518
Jens Palsberg and
Scott Smith Constrained types and their
expressiveness . . . . . . . . . . . . . 519--527
Steven Dawson and
C. R. Ramakrishnan and
Steven Skiena and
Terrance Swift Principles and practice of unification
factoring . . . . . . . . . . . . . . . 528--563
M. Garcia de la Banda and
M. Hermenegildo and
M. Bruynooghe and
V. Dumortier and
G. Janssens and
W. Simoens Global analysis of constraint logic
programs . . . . . . . . . . . . . . . . 564--614
M. Garcia De La Banda and
M. Hermenegildo and
M. Bruynooghe and
V. Dumortier and
G. Janssens and
W. Simoens Global analysis of constraint logic
programs . . . . . . . . . . . . . . . . 564--614
José M. Piquer Indirect distributed garbage collection:
Handling object migration . . . . . . . 615--647
Vugranam C. Sreedhar and
Guang R. Gao and
Yong-Fong Lee Identifying loops using DJ graphs . . . 649--658
Jonas Skeppstedt and
Per Stenström Using dataflow analysis techniques to
reduce ownership overhead in cache
coherence protocols . . . . . . . . . . 659--682
Todd A. Proebsting and
Charles N. Fischer Demand-driven register allocation . . . 683--710
Isabelle Attali and
Denis Caromel and
Sidi Ould Ehmety A natural semantics for Eiffel dynamic
binding . . . . . . . . . . . . . . . . 711--729
Olivier Danvy and
Karoline Malmkjær and
Jens Palsberg Eta-expansion does the trick . . . . . . 730--751
Neng-Fa Zhou Parameter passing and control stack
management in Prolog implementation
revisited . . . . . . . . . . . . . . . 752--779
Susan Horwitz Precise Flow-Insensitive May-Alias
Analysis is NP-Hard . . . . . . . . . . 1--6
Agostino Cortesi and
Gilberto File and
Roberto Giacobazzi and
Catuscia Palamidessi and
Francesco Ranzato Complementation in Abstract
Interpretation . . . . . . . . . . . . . 7--47
Paul A. Steckler and
Mitchell Wand Lightweight Closure Conversion . . . . . 48--86
Andrew K. Wright and
Robert Cartwright A Practical Soft Type System for Scheme 87--152
Gerald Baumgartner and
Vincent F. Russo Implementing Signatures for C++ . . . . 153--187
Brad Calder and
Dirk Grunwald and
Michael Jones and
Donald Lindsay and
James Martin and
Michael Mozer and
Benjamin Zorn Evidence-Based Static Branch Prediction
Using Machine Learning . . . . . . . . . 188--222
Nicholas Pippenger Pure versus impure Lisp . . . . . . . . 223--238
Vugranam C. Sreedhar and
Guang R. Gao and
Yong-Fong Lee Incremental computation of dominator
trees . . . . . . . . . . . . . . . . . 239--252
Dennis Dams and
Rob Gerth and
Orna Grumberg Abstract interpretation of reactive
systems . . . . . . . . . . . . . . . . 253--291
Daniel M. Yellin and
Robert E. Strom Protocol specifications and component
adaptors . . . . . . . . . . . . . . . . 292--333
Patrick M. Sansom and
Simon L. Peyton Jones Formally based profiling for
higher-order functional languages . . . 334--385
Jin Yang and
Aloysius K. Mok and
Farn Wang Symbolic model checking for event-driven
real-time systems . . . . . . . . . . . 386--412
Charles L. A. Clarke and
Gordon V. Cormack On the use of Regular Expressions for
Searching Text . . . . . . . . . . . . . 413--426
Dexter Kozen Kleene Algebra with Tests . . . . . . . 427--443
Zhenjiang Hu and
Hideya Iwasaki and
Masato Takechi Formal Derivation of Efficient Parallel
Programs by Construction of List
Homomorphisms . . . . . . . . . . . . . 444--461
Keshav Pingali and
Gianfranco Bilardi Optimal Control Dependence Computation
and the Roman Chariots Problem . . . . . 462--491
Norman Ramsey and
Mary F. Fernández Specifying Representations of Machine
Instructions . . . . . . . . . . . . . . 492--524
Richard Gerber and
Seongsoo Hong Slicing real-time programs for enhanced
schedulability . . . . . . . . . . . . . 525--555
Paul Havlak Nesting of Reducible and Irreducible
Loops . . . . . . . . . . . . . . . . . 557--567
Saumya K. Debray and
Todd A. Proebsting Interprocedural Control Flow Analysis of
First-Order Programs with Tail-Call
Optimization . . . . . . . . . . . . . . 568--585
Peter T. Breuer and
Carlos Delgado Kloos and
Andrés Marín López and
Natividad Martínez Madrid and
Luis Sánchez Fernández A Refinement Calculus for the Synthesis
of Verified Hardware Descriptions in
VHDL . . . . . . . . . . . . . . . . . . 586--616
E. A. Emerson and
A. P. Sistla Utilizing Symmetry when Model-Checking
under Fairness Assumptions: An
Automata-Theoretic Approach . . . . . . 617--638
J. A. Bergstra and
T. B. Dinesh and
J. Field and
J. Heering Toward a Complete Transformational
Toolkit for Compilers . . . . . . . . . 639--684
Frank S. De Boer and
Maurizio Gabbrielli and
Elena Marchiori and
Catuscia Palamidessi Proving Concurrent Constraint Programs
Correct . . . . . . . . . . . . . . . . 685--725
E. M. Clarke and
O. Grumberg and
S. Jha Verifying Parameterized Networks . . . . 726--750
Thomas Jensen Disjunctive Program Analysis for
Algebraic Data Types . . . . . . . . . . 751--803
Peter Van Roy and
Seif Haridi and
Per Brand and
Gert Smolka and
Michael Mehl and
Ralf Scheidhauer Mobile Objects in Distributed Oz . . . . 804--851
Soo-Mook Moon and
Kemal Ebcio\uglu Parallelizing nonnumerical code with
selective scheduling and software
pipelining . . . . . . . . . . . . . . . 853--898
N. Raja and
R. K. Shyamasundar Combinatory formulations of concurrent
languages . . . . . . . . . . . . . . . 899--915
Amr Sabry and
Philip Wadler A reflection on a call-by-value . . . . 916--941
Martin C. Rinard and
Pedro C. Diniz Commutativity analysis: a new analysis
technique for parallelizing compilers 942--991
Evelyn Duesterwald and
Rajiv Gupta and
Mary Lou Soffa A practical framework for demand-driven
interprocedural data flow analysis . . . 992--1030
Johan Janssen and
Henk Corporaal Making graphs reducible with controlled
node splitting . . . . . . . . . . . . . 1031--1052
Deborah L. Whitfield and
Mary Lou Soffa An approach for exploring code improving
transformations . . . . . . . . . . . . 1053--1084
Ting Yu and
Owen Kaser A note on ``On the conversion of
indirect to direct recursion'' . . . . . 1085--1087
Mooly Sagiv and
Thomas Reps and
Reinhard Wilhelm Solving shape-analysis problems in
languages with destructive updating . . 1--50
Paul C. Attie and
E. Allen Emerson Synthesis of concurrent systems with
many similar processes . . . . . . . . . 51--115
Eric Dujardin and
Eric Amiel and
Eric Simon Fast algorithms for compressed
multimethod dispatch table generation 116--165
Andrew K. Wright and
Suresh Jagannathan Polymorphic splitting: an effective
polyvariant flow analysis . . . . . . . 166--207
Michael Leuschel and
Bern Martens and
Danny De Schreye Controlling generalization and
polyvariance in partial deduction of
normal logic programs . . . . . . . . . 208--258
Thomas Reps ``Maximal-munch'' tokenization in linear
time . . . . . . . . . . . . . . . . . . 259--273
Jun Lang and
David B. Stewart A study of the applicability of existing
exception-handling techniques to
component-base real-time software
technology . . . . . . . . . . . . . . . 274--301
Daniel Jackson and
Somesh Jha and
Craig A. Damon Isomorph-free model enumeration: a new
method for checking relational
specifications . . . . . . . . . . . . . 302--343
Rémi Douence and
Pascal Fradet A systematic study of functional
language implementations . . . . . . . . 344--387
Vugranam C. Sreedhar and
Guang R. Gao and
Yong-Fong Lee A New Framework for Elimination-Based
Data Flow Analysis Using DJ Graphs . . . 388--435
Naoki Kobayashi A Partially Deadlock-Free Typed Process
Calculus . . . . . . . . . . . . . . . . 436--482
Martin C. Rinard and
Monica S. Lam The Design, Implementation, and
Evaluation of Jade . . . . . . . . . . . 483--545
Yanhong A. Liu and
Scott D. Stoller and
Tim Teitelbaum Static Caching for Incremental
Computation . . . . . . . . . . . . . . 546--585
Konstantinos Sagonas and
Terrance Swift An Abstract Machine for Tabled Execution
of Fixed-Order Stratified Logic Programs 586--634
William Pugh and
David Wonnacott Constraint-Based Array Dependence
Analysis . . . . . . . . . . . . . . . . 635--678
Wan Fokkink and
Jasper Kamperman and
Pum Walters Within ARM's Reach: Compilation of
Left-Linear Rewrite Systems via Minimal
Rewrite Systems . . . . . . . . . . . . 679--706
Oukseh Lee and
Kwangkeun Yi Proofs about a Folklore Let-Polymorphic
Type Inference Algorithm . . . . . . . . 707--723
Mads Tofte and
Lars Birkedal A Region Inference Algorithm . . . . . . 724--767
María Alpuente and
Moreno Falaschi and
Germán Vidal Partial Evaluation of Functional Logic
Programs . . . . . . . . . . . . . . . . 768--844
J. Michael Ashley and
R. Kent Dybvig A Practical and Flexible Flow Analysis
for Higher-Order Languages . . . . . . . 845--868
Ken Kennedy and
Ulrich Kremer Automatic Data Layout for
Distributed-Memory Machines . . . . . . 869--916
Eric Y. T. Juan and
Jeffrey J. P. Tsai and
Tadao Murata Compositional Verification of Concurrent
Systems Using Petri-Net-Based
Condensation Rules . . . . . . . . . . . 917--979
Tim A. Wagner and
Susan L. Graham Efficient and Flexible Incremental
Parsing . . . . . . . . . . . . . . . . 980--1013
Krzsztof R. Apt and
Jacob Brunekreef and
Vincent Partington and
Andrea Schaerf Alma-O: An Imperative Language that
Supports Declarative Programming . . . . 1014--1066
Roberto Giacobazzi and
Francesca Scozzari A Logical Model for Relational Abstract
Domains . . . . . . . . . . . . . . . . 1067--1109
D. M. Dhamdhere and
K. V. Sankaranarayanan Dynamic currency determination in
optimized programs . . . . . . . . . . . 1111--1130
Saniya Ben Hassen and
Henri E. Bal and
Ceriel J. H. Jacobs A task- and data-parallel programming
language based on shared objects . . . . 1131--1170
Rajeev Alur and
Thomas A. Henzinger Finitary fairness . . . . . . . . . . . 1171--1194
Tao Yang and
Cong Fu Space/time-efficient scheduling and
execution of parallel irregular
computations . . . . . . . . . . . . . . 1195--1222
Andrew D. Kelly and
Kim Marriott and
Andrew MacDonald and
Peter J. Stuckey and
Roland Yap Optimizing compilation of CLP(\cal R) 1223--1250
Jens Palsberg Equality-based flow analysis versus
recursive types . . . . . . . . . . . . 1251--1264
Adam L. Buchsbaum and
Haim Kaplan and
Anne Rogers and
Jeffery R. Westbrook A new, simpler linear-time dominators
algorithm . . . . . . . . . . . . . . . 1265--1296
Max Hailperin Cost-optimal code motion . . . . . . . . 1297--1322
Anonymous 1998 Author Index . . . . . . . . . . . 1323--1325
Eberhard Bertsch and
Mark-Jan Nederhof On Failure of the Pruning Technique in
``Error Repair in Shift-Reduce Parsers'' 1--10
Dominic Duggan Dynamic Typing for Distributed
Programming in Polymorphic Languages . . 11--45
Zhiming Liu and
Mathai Joseph Specification and Verification of
Fault-Tolerance, Timing, and Scheduling 46--89
Raymie Stata and
Martin Abadi A Type System for Java Bytecode
Subroutines . . . . . . . . . . . . . . 90--137
Girija J. Narlikar and
Guy E. Blelloch Space-Efficient Scheduling of Nested
Parallelism . . . . . . . . . . . . . . 138--173
G. Ramalingam Identifying loops in almost linear time 175--188
Francisco Bueno and
María García de la Banda and
Manuel Hermenegildo Effectiveness of abstract interpretation
in automatic parallelization: a case
study in logic programming . . . . . . . 189--239
John Greiner and
Guy E. Blelloch A provably time-efficient parallel
implementation of full speculation . . . 240--285
Luiz De Rose and
David Padua Techniques for the translation of MATLAB
programs into Fortran 90 . . . . . . . . 286--323
Massimiliano Poletto and
Wilson C. Hsieh and
Dawson R. Engler and
M. Frans Kaashoek 'C and \tt tcc: a language and compiler
for dynamic code generation . . . . . . 324--369
Cormac Flanagan and
Matthias Felleisen Componential set-based analysis . . . . 370--416
Michael Butler and
Pieter Hartel Reasoning about Grover's quantum search
algorithm using probabilistic \em wp . . 417--429
Gudjón Gudjónsson and
William H. Winsborough Compile-time memory reuse in logic
programming languages through update in
place . . . . . . . . . . . . . . . . . 430--501
Leslie Lamport and
Lawrence C. Paulson Should your specification language be
typed . . . . . . . . . . . . . . . . . 502--526
Greg Morrisett and
David Walker and
Karl Crary and
Neal Glew From System F to typed assembly language 527--568
Seif Haridi and
Peter Van Roy and
Per Brand and
Michael Mehl and
Ralf Scheidhauer and
Gert Smolka Efficient logic variables for
distributed computing . . . . . . . . . 569--626
Robert Kennedy and
Sun Chan and
Shin-Ming Liu and
Raymond Lo and
Peng Tu and
Fred Chow Partial redundancy elimination in SSA
form . . . . . . . . . . . . . . . . . . 627--676
J. M. Morris and
A. Bunkenburg Specificational functions . . . . . . . 677--701
Somnath Ghosh and
Margaret Martonosi and
Sharad Malik Cache miss equations: a compiler
framework for analyzing and tuning
memory behavior . . . . . . . . . . . . 703--746
Tevfik Bultan and
Richard Gerber and
William Pugh Model-checking concurrent systems with
unbounded integer variables: symbolic
representations, approximations, and
experimental results . . . . . . . . . . 747--789
Matthias Blume Dependency analysis for Standard ML . . 790--812
Matthias Blume and
Andrew W. Appel Hierarchical modularity . . . . . . . . 813--847
Michael Hind and
Michael Burke and
Paul Carini and
Jong-Deok Choi Interprocedural pointer alias analysis 848--894
Massimiliano Poletto and
Vivek Sarkar Linear scan register allocation . . . . 895--913
Naoki Kobayashi and
Benjamin C. Pierce and
David N. Turner Linearity and the Pi-Calculus . . . . . 914--947
Michael Codish and
Harald Sòndergaard and
Peter J. Stuckey Sharing and groundness dependencies in
logic programs . . . . . . . . . . . . . 948--976
Nikolas Gloy and
Michael D. Smith Procedure placement using
temporal-ordering information . . . . . 977--1027
Cliff Young and
Michael D. Smith Static correlated branch prediction . . 1028--1075
P. Bottoni and
M. F. Costabile and
P. Mussio Specification and dialogue control of
visual interaction through visual
rewriting systems . . . . . . . . . . . 1077--1136
Stefaan Decorte and
Danny De Schreye and
Henk Vandecasteele Constraint-based termination analysis of
logic programs . . . . . . . . . . . . . 1137--1195
Stephen N. Freund and
John C. Mitchell The type system for object
initialization in the Java bytecode
language . . . . . . . . . . . . . . . . 1196--1250
M. Kandemir and
P. Banerjee and
A. Choudhary and
J. Ramanujam and
N. Shenoy A global communication optimization
technique based on data-flow analysis
and linear algebra . . . . . . . . . . . 1251--1297
Benjamin C. Pierce and
David N. Turner Local type inference . . . . . . . . . . 1--44
Wan Fokkink and
Jasper Kamperman and
Pum Walters Lazy rewriting on eager machinery . . . 45--86
Orna Kuperman and
Moshe Y. Vardi An automata-theoretic approach to
modular model checking . . . . . . . . . 87--128
Zhong Shao and
Andrew W. Appel Efficient and safe-for-space closure
conversion . . . . . . . . . . . . . . . 129--161
Thomas Reps Undecidability of context-sensitive
data-independence analysis . . . . . . . 162--186
Manuel Hermenegildo and
German Puebla and
Kim Marriott and
Peter J. Stuckey Incremental analysis of constraint logic
programs . . . . . . . . . . . . . . . . 187--223
Michael Sperber and
Peter Thiemann Generation of LR parsers by partial
evaluation . . . . . . . . . . . . . . . 224--264
José E. Moreira and
Samuel P. Midkiff and
Manish Gupta From flop to megaflops: Java for
technical computing . . . . . . . . . . 265--295
Marí García De La Banda and
Manuel Hermengildo and
Kim Marriott Independence in CLP languages . . . . . 296--339
Xavier Leroy and
François Pessaux Type-based analysis of uncaught
exceptions . . . . . . . . . . . . . . . 340--377
Saumya K. Debray and
William Evans and
Robert Muth and
Bjorn De Sutter Compiler techniques for code compaction 378--415
G. Ramalingam Context-sensitive
synchronization-sensitive analysis is
undecidable . . . . . . . . . . . . . . 416--430
Guei-Yuan Lueh and
Thomas Gross and
Ali-Reza Adl-Tabatabai Fusion-based register allocation . . . . 431--470
Lars Ræder Clausen and
Ulrik Pagh Schultz and
Charles Consel and
Gilles Muller Java bytecode compression for low-end
embedded systems . . . . . . . . . . . . 471--489
Thomas Kistler and
Michael Franz Automated data-member layout of heap
objects to improve memory-hierarchy
performance . . . . . . . . . . . . . . 490--505
A. J. Wellings and
B. Johnson and
B. Sanden and
J. Kienzle and
T. Wolf and
S. Michell Integrating object-oriented programming
and protected objects in Ada 95 . . . . 506--539
Gregor Snelting and
Frank Tip Understanding class hierarchies using
concept analysis . . . . . . . . . . . . 540--582
Uwe Assmann Graph rewrite systems for program
optimization . . . . . . . . . . . . . . 583--637
Zhenyu Qian Standard fixpoint iteration for Java
bytecode verification . . . . . . . . . 638--672
Hong Tang and
Kai Shen and
Tao Yang Program transformation and runtime
support for threaded MPI execution on
shared-memory machines . . . . . . . . . 673--700
David Walker and
Karl Crary and
Greg Morrisett Typed memory management via static
capabilities . . . . . . . . . . . . . . 701--771
Fabien Quilleré and
Sanjay Rajopadhye Optimizing memory usage in the
polyhedral model . . . . . . . . . . . . 773--815
Reinhard von Hanxleden and
Ken Kennedy A balanced code placement framework . . 816--860
Agostino Dovier and
Carla Piazza and
Enrico Pontelli and
Gianfranco Rossi Sets and constraint logic programming 861--931
Brian Grant and
Markus Mock and
Matthai Philipose and
Craig Chambers and
Susan J. Eggers The benefits and costs of DyC's run-time
optimizations . . . . . . . . . . . . . 932--972
Maya Madhavan and
Priti Shankar and
Siddhartha Rai and
U. Ramakrishna Extending Graham-Glanville techniques
for optimal code generation . . . . . . 973--1001
Krzysztof R. Apt The role of commutativity in constraint
propagation algorithms . . . . . . . . . 1002--1036
Dan Grossman and
Greg Morrisett and
Steve Zdancewic Syntactic type abstraction . . . . . . . 1037--1080
Stefano Bistarelli and
Ugo Montanari and
Francesca Rossi Semiring-based constraint logic
programming: syntax and semantics . . . 1--29
Amer Diwan and
Kathryn S. McKinley and
J. Eliot B. Moss Using types to analyze and optimize
object-oriented programs . . . . . . . . 30--72
Allen Leung and
Krishna V. Palem and
Amir Pnueli Scheduling time-constrained instructions
on pipelined processors . . . . . . . . 73--103
Barbara G. Ryder and
William A. Landi and
Philip A. Stocks and
Sean Zhang and
Rita Altucher A schema for interprocedural
modification side-effect analysis with
pointer aliasing . . . . . . . . . . . . 105--186
Paul C. Attie and
E. Allen Emerson Synthesis of concurrent programs for an
atomic read/write model of computation 187--242
Todd B. Knoblock and
Jakob Rehof Type elaboration and subtype completion
for Java bytecode . . . . . . . . . . . 243--272
Rajeev Alur and
Mihalis Yannakakis Model checking of hierarchical state
machines . . . . . . . . . . . . . . . . 273--303
Sandro Etalle and
Maurizio Gabbrielli and
Maria Chiara Meo Transformations of CCP programs . . . . 304--395
Atsushi Igarashi and
Benjamin C. Pierce and
Philip Wadler Featherweight Java: a minimal core
calculus for Java and GJ . . . . . . . . 396--450
Ik-Soon Kim and
Kwang-Moo Choe Error repair with validation in LR-based
parsing . . . . . . . . . . . . . . . . 451--471
Gopal Gupta and
Enrico Pontelli and
Khayri A. M. Ali and
Mats Carlsson and
Manuel V. Hermenegildo Parallel execution of Prolog programs: a
survey . . . . . . . . . . . . . . . . . 472--602
Keith D. Cooper and
L. Taylor Simpson and
Christopher A. Vick Operator strength reduction . . . . . . 603--625
Lawrence C. Paulson Mechanizing a theory of program
composition for UNITY . . . . . . . . . 626--656
Andrew W. Appel and
David McAllester An indexed model of recursive types for
foundational proof-carrying code . . . . 657--683
David Grove and
Craig Chambers A framework for call graph construction
algorithms . . . . . . . . . . . . . . . 685--746
Jason Maassen and
Rob Van Nieuwpoort and
Ronald Veldema and
Henri Bal and
Thilo Kielmann and
Ceriel Jacobs and
Rutger Hofman Efficient Java RMI for parallel
programming . . . . . . . . . . . . . . 747--775
Bradley T. Vander Zanden and
Richard Halterman and
Brad A. Myers and
Rich McDaniel and
Rob Miller and
Pedro Szekely and
Dario A. Giuse and
David Kosbie Lessons learned about one-way, dataflow
constraints in the Garnet and Amulet
graphical toolkits . . . . . . . . . . . 776--796
Peizong Lee and
Zvi Meir Kedem Automatic data and computation
decomposition on distributed memory
parallel computers . . . . . . . . . . . 1--50
Thomas A. Henzinger and
Shaz Qadeer and
Sriram K. Rajamani and
Serdar Tasiran An assume-guarantee rule for checking
simulation . . . . . . . . . . . . . . . 51--64
Yunheung Paek and
Jay Hoeflinger and
David Padua Efficient and precise array access
analysis . . . . . . . . . . . . . . . . 65--109
Kathleen Fisher and
Benjamin C. Pierce Guest editorial . . . . . . . . . . . . 111--111
Christopher League and
Zhong Shao and
Valery Trifonov Type-preserving compilation of
Featherweight Java . . . . . . . . . . . 112--152
Sophia Drossopoulou and
Ferruccio Damiani and
Mariangiola Dezani-Ciancaglini and
Paola Giannini More dynamic object reclassification:
\em Fickle$_\parallel $ . . . . . . . . 153--191
J. Strother Moore and
George Porter The apprentice challenge . . . . . . . . 193--216
Mooly Sagiv and
Thomas Reps and
Reinhard Wilhelm Parametric shape analysis via $3$-valued
logic . . . . . . . . . . . . . . . . . 217--298
Sebastian Unger and
Frank Mueller Handling irreducible loops: optimized
node splitting versus DJ-graphs . . . . 299--333
M. G. J. Van Den Brand and
J. Heering and
P. Klint and
P. A. Olivier Compiling language definitions: the
ASF+SDF compiler . . . . . . . . . . . . 334--368
Anonymous Automatic derivation of compiler machine
descriptions . . . . . . . . . . . . . . 369--408
Marta Jiménez and
José M. Llabería and
Agustín Fernández Register tiling in nonrectangular
iteration spaces . . . . . . . . . . . . 409--453
Anonymous On loops, dominators, and dominance
frontiers . . . . . . . . . . . . . . . 455--490
K. Rustan M. Leino and
Greg Nelson Data abstraction and information hiding 491--553
Arthur Charlesworth The undecidability of associativity and
commutativity analysis . . . . . . . . . 554--565
Matthew Hennessy and
James Riely Information flow vs. resource access in
the asynchronous pi-calculus . . . . . . 566--591
Martin Hirzel and
Amer Diwan and
Johannes Henkel On the usefulness of type and liveness
accuracy for garbage collection and leak
detection . . . . . . . . . . . . . . . 593--624
Frank Tip and
Peter F. Sweeney and
Chris Laffra and
Aldo Eisma and
David Streeter Practical extraction techniques for Java 625--666
Minghui Yang and
Gang-Ryung Uh and
David B. Whalley Efficient and effective branch
reordering using profile data . . . . . 667--697
Rafael Corchuelo and
José A. Pérez and
Antonio Ruiz and
Miguel Toro Repairing syntax errors in LR parsers 698--710
Dominic Duggan Type-Safe linking with recursive DLLs
and shared libraries . . . . . . . . . . 711--804
Francesca Levi and
Davide Sangiorgi Mobile safe ambients . . . . . . . . . . 1--69
Radu Rugina and
Martin C. Rinard Pointer analysis for structured parallel
programs . . . . . . . . . . . . . . . . 70--116
François Pottier and
Vincent Simonet Information flow inference for ML . . . 117--158
Bratin Saha and
Valery Trifonov and
Zhong Shao Intensional analysis of quantified types 159--209
Norman Ramsey and
Cristina Cifuentes A transformational approach to binary
translation of delayed branches . . . . 210--224
Kim B. Bruce and
Angela Schuett and
Robert van Gent and
Adrian Fiech PolyTOIL: a type-safe polymorphic
object-oriented language . . . . . . . . 225--290
Morten Rhiger A foundation for embedded languages . . 291--315
Martin C. Rinard and
Pedro C. Diniz Eliminating synchronization bottlenecks
using adaptive replication . . . . . . . 316--359
Cedric Fournet and
Andrew D. Gordon Stack inspection: Theory and variants 360--399
Ferruccio Damiani Rank $2$ intersection types for local
definitions and conditional expressions 401--451
Ulrik P. Schultz and
Julia L. Lawall and
Charles Consel Automatic program specialization for
Java . . . . . . . . . . . . . . . . . . 452--499
Thomas Kistler and
Michael Franz Continuous program optimization: a case
study . . . . . . . . . . . . . . . . . 500--548
Roberto M. Amadio and
Gérard Boudol and
Cédric Lhoussaine The receptive distributed $ \pi
$-calculus . . . . . . . . . . . . . . . 549--577
Fausto Spoto and
Thomas Jensen Class analyses as abstract
interpretations of trace semantics . . . 578--630
Clinton L. Jeffery Generating LR syntax error messages from
examples . . . . . . . . . . . . . . . . 631--640
Davide Ancona and
Giovanni Lagorio and
Elena Zucca Jam---designing a Java extension with
mixins . . . . . . . . . . . . . . . . . 641--712
Bruno Blanchet Escape analysis for Java$^{TM}$: Theory
and practice . . . . . . . . . . . . . . 713--775
Vijay Menon and
Keshav Pingali and
Nikolay Mateev Fractal symbolic analysis . . . . . . . 776--813
Aske Simon Christensen and
Anders Mòller and
Michael I. Schwartzbach Extending Java for high-level Web
service construction . . . . . . . . . . 814--875
Jong-Deok Choi and
Manish Gupta and
Mauricio J. Serrano and
Vugranam C. Sreedhar and
Samuel P. Midkiff Stack allocation and synchronization
optimizations for Java using escape
analysis . . . . . . . . . . . . . . . . 876--910
Antonio J. Fernández and
Patricia M. Hill An interval constraint system for
lattice domains . . . . . . . . . . . . 1--46
Sergei Gorlatch Send-receive considered harmful: Myths
and realities of message passing . . . . 47--56
Michele Bugliesi and
Giuseppe Castagna and
Silvia Crafa Access control for mobile agents: The
calculus of boxed ambients . . . . . . . 57--124
Paul C. Attie and
Anish Arora and
E. Allen Emerson Synthesis of fault-tolerant concurrent
programs . . . . . . . . . . . . . . . . 125--185
Pei-Chi Wu On exponential-time completeness of the
circularity problem for attribute
grammars . . . . . . . . . . . . . . . . 186--190
Niels H. Christensen and
Robert Glück Offline partial evaluation can be as
accurate as online partial evaluation 191--220
Yifeng Chen and
J. W. Sanders Logic of global synchrony . . . . . . . 221--262
Xavier Vera and
Nerina Bermudo and
Josep Llosa and
Antonio González A fast and accurate framework to analyze
and optimize cache memory behavior . . . 263--300
Corinna Cortes and
Kathleen Fisher and
Daryl Pregibon and
Anne Rogers and
Frederick Smith Hancock: a language for analyzing
transactional data streams . . . . . . . 301--338
Rajeev Alur and
Radu Grosu Modular refinement of hierarchic
reactive machines . . . . . . . . . . . 339--369
Karl Lieberherr and
Boaz Patt-Shamir and
Doug Orleans Traversals of object structures:
Specification and efficient
implementation . . . . . . . . . . . . . 370--412
Michael Leuschel A framework for the integration of
partial evaluation and abstract
interpretation of logic programs . . . . 413--463
Abhik Roychoudhury and
K. Narayan Kumar and
C. R. Ramakrishnan and
I. V. Ramakrishnan An unfold/fold transformation framework
for definite logic programs . . . . . . 464--509
Sabine Glesner and
Wolf Zimmermann Natural semantics as a static program
analysis framework . . . . . . . . . . . 510--577
Aaron W. Keen and
Tingjian Ge and
Justin T. Maris and
Ronald A. Olsson JR: Flexible distributed programming in
an extended Java . . . . . . . . . . . . 578--608
Rajiv Mirani and
Paul Hudak First-class monadic schedules . . . . . 609--651
Simon Helsen and
Peter Thiemann Polymorphic specialization for ML . . . 652--701
A. Prasad Sistla and
Patrice Godefroid Symmetry and reduced symmetry in model
checking . . . . . . . . . . . . . . . . 702--734
Jinpyo Park and
Soo-Mook Moon Optimistic register coalescing . . . . . 735--765
Martin Odersky and
Benjamin C. Pierce Guest editorial . . . . . . . . . . . . 767--768
Nick Benton and
Luca Cardelli and
Cédric Fournet Modern concurrency abstractions for C# 769--804
Christopher A. Stone Extensible objects without labels . . . 805--835
Todd Millstein and
Colin Bleckner and
Craig Chambers Modular typechecking for hierarchically
extensible datatypes and functions . . . 836--889
Mitchell Wand and
Gregor Kiczales and
Christopher Dutchyn A semantics for advice and dynamic join
points in aspect-oriented programming 890--910
C. Barry Jay The pattern calculus . . . . . . . . . . 911--937
Sathyanarayanan Thammanur and
Santosh Pande A fast, memory-efficient register
allocation framework for embedded
systems . . . . . . . . . . . . . . . . 938--974
Zhiyuan Li and
Yonghong Song Automatic tiling of iterative stencil
loops . . . . . . . . . . . . . . . . . 975--1028
John Clements and
Matthias Felleisen A tail-recursive machine with stack
inspection . . . . . . . . . . . . . . . 1029--1052
Zhong Shao and
Valery Trifonov and
Bratin Saha and
Nikolaos Papaspyrou A type system for certified binaries . . 1--45
Haruo Hosoya and
Jérôme Vouillon and
Benjamin C. Pierce Regular expression types for XML . . . . 46--90
Yanhong A. Liu and
Scott D. Stoller and
Ning Li and
Tom Rothamel Optimizing aggregate array computations
in loops . . . . . . . . . . . . . . . . 91--125
Jens Palsberg and
Tian Zhao and
Trevor Jim Automatic discovery of covariant
read-only fields . . . . . . . . . . . . 126--162
Olaf Chitil Pretty printing with lazy dequeues . . . 163--184
Radu Rugina and
Martin C. Rinard Symbolic bounds analysis of pointers,
array indices, and accessed memory
regions . . . . . . . . . . . . . . . . 185--235
Marco Gavanelli and
Evelina Lamma and
Paola Mello and
Michela Milano Dealing with incomplete knowledge on
CLP(\em FD) variable domains . . . . . . 236--263
Atsushi Igarashi and
Naoki Kobayashi Resource usage analysis . . . . . . . . 264--313
Thomas Ball and
Todd Millstein and
Sriram K. Rajamani Polymorphic predicate abstraction . . . 314--343
François Pottier and
Christian Skalka and
Scott Smith A systematic approach to static access
control . . . . . . . . . . . . . . . . 344--382
Adam L. Buchsbaum and
Haim Kaplan and
Anne Rogers and
Jeffery R. Westbrook Corrigendum: ``A new, simpler
linear-time dominators algorithm'' . . . 383--387
Christian Schulte and
Peter J. Stuckey When do bounds and domain propagation
lead to the same search space? . . . . . 388--425
Dibyendu Das and
U. Ramakrishna A practical and fast iterative algorithm
for $ \phi $-function computation using
DJ graphs . . . . . . . . . . . . . . . 426--440
Luc Moreau and
Christian Queinnec Resource aware programming . . . . . . . 441--476
George C. Necula and
Jeremy Condit and
Matthew Harren and
Scott McPeak and
Westley Weimer CCured: type-safe retrofitting of legacy
software . . . . . . . . . . . . . . . . 477--526
Thi Viet Nga Nguyen and
François Irigoin Efficient and effective array bound
checking . . . . . . . . . . . . . . . . 527--570
Max Hailperin Comparing conservative coalescing
criteria . . . . . . . . . . . . . . . . 571--582
Godmar Back and
Wilson C. Hsieh The KaffeOS Java runtime system . . . . 583--630
Xiangyu Zhang and
Rajiv Gupta and
Youtao Zhang Cost and precision tradeoffs of dynamic
data slicing algorithms . . . . . . . . 631--661
Mary W. Hall and
Saman P. Amarasinghe and
Brian R. Murphy and
Shih-Wei Liao and
Monica S. Lam Interprocedural parallelization analysis
in SUIF . . . . . . . . . . . . . . . . 662--731
Toshio Suganuma and
Toshiaki Yasue and
Motohiro Kawahito and
Hideaki Komatsu and
Toshio Nakatani Design and evaluation of dynamic
optimizations for a Java just-in-time
compiler . . . . . . . . . . . . . . . . 732--785
Rajeev Alur and
Michael Benedikt and
Kousha Etessami and
Patrice Godefroid and
Thomas Reps and
Mihalis Yannakakis Analysis of recursive state machines . . 786--818
Joseph (Yossi) Gil and
Yoav Zibin Efficient subtyping tests with
PQ-encoding . . . . . . . . . . . . . . 819--856
Tom Hirschowitz and
Xavier Leroy Mixin modules in a call-by-value setting 857--881
Bjorn De Sutter and
Bruno De Bus and
Koen De Bosschere Link-time binary rewriting techniques
for program compaction . . . . . . . . . 882--945
Xavier Vera and
Jaume Abella and
Josep Llosa and
Antonio González An accurate cost model for guiding data
locality transformations . . . . . . . . 946--987
Raymond Boute Functional declarative language design
and predicate calculus: a practical
approach . . . . . . . . . . . . . . . . 988--1047
Michael Hicks and
Scott Nettles Dynamic software updating . . . . . . . 1049--1096
Katherine Barabash and
Ori Ben-Yitzhak and
Irit Goft and
Elliot K. Kolodner and
Victor Leikehman and
Yoav Ossia and
Avi Owshanko and
Erez Petrank A parallel, incremental, mostly
concurrent garbage collector for servers 1097--1146
Arne John Glenstrup and
Neil D. Jones Termination analysis and
specialization-point insertion in
offline partial evaluation . . . . . . . 1147--1215
Peter J. Stuckey and
Martin Sulzmann A theory of overloading . . . . . . . . 1216--1269
Peter A. Buhr and
Ashif S. Harji Implicit-signal monitors . . . . . . . . 1270--1343
Luc Moreau and
Peter Dickman and
Richard Jones Birrell's distributed reference listing
revisited . . . . . . . . . . . . . . . 1344--1395
Yossi Levanoni and
Erez Petrank An on-the-fly reference-counting garbage
collector for Java . . . . . . . . . . . 1--69
Takeshi Ogasawara and
Hideaki Komatsu and
Toshio Nakatani EDO: Exception-Directed Optimization in
Java . . . . . . . . . . . . . . . . . . 70--105
Motohiro Kawahito and
Hideaki Komatsu and
Toshio Nakatani Effective sign extension elimination for
Java . . . . . . . . . . . . . . . . . . 106--133
Toshio Suganuma and
Toshiaki Yasue and
Toshio Nakatani A region-based compilation technique for
dynamic compilers . . . . . . . . . . . 134--174
Kevin W. Hamlen and
Greg Morrisett and
Fred B. Schneider Computability classes for enforcement
mechanisms . . . . . . . . . . . . . . . 175--205
Martin Abadi and
Cormac Flanagan and
Stephen N. Freund Types for safe locking: Static race
detection for Java . . . . . . . . . . . 207--255
Etienne Payet and
Fred Mesnard Nontermination inference of logic
programs . . . . . . . . . . . . . . . . 256--289
Massimo Merro and
Matthew Hennessy A bisimulation-based semantic theory of
Safe Ambients . . . . . . . . . . . . . 290--330
Stéphane Ducasse and
Oscar Nierstrasz and
Nathanael Schärli and
Roel Wuyts and
Andrew P. Black Traits: a mechanism for fine-grained
reuse . . . . . . . . . . . . . . . . . 331--388
Stijn Vansummeren Type inference for unique pattern
matching . . . . . . . . . . . . . . . . 389--428
Dan Grossman Quantified types in an imperative
language . . . . . . . . . . . . . . . . 429--475
Matthew Hertz and
Stephen M. Blackburn and
J. Eliot B. Moss and
Kathryn S. McKinley and
Darko Stefanovi\'c Generating object lifetime traces with
Merlin . . . . . . . . . . . . . . . . . 476--516
Curtis Clifton and
Todd Millstein and
Gary T. Leavens and
Craig Chambers MultiJava: Design rationale, compiler
implementation, and applications . . . . 517--575
Elizabeth Scott and
Adrian Johnstone Right nulled GLR parsers . . . . . . . . 577--618
Gerwin Klein and
Tobias Nipkow A machine-checked model for a Java-like
language, virtual machine, and compiler 619--695
Mads Sig Ager and
Olivier Danvy and
Henning Korsholm Rohde Fast partial evaluation of pattern
matching in strings . . . . . . . . . . 696--714
Richard Carlsson and
Konstantinos Sagonas and
Jesper Wilhelmsson Message analysis for concurrent programs
using message passing . . . . . . . . . 715--746
Raymond T. Boute Calculational semantics: Deriving
programming theories from equations by
functional predicate calculus . . . . . 747--793
Atsushi Igarashi and
Mirko Viroli Variant parametric types: a flexible
subtyping scheme for generics . . . . . 795--847
Pramod G. Joisha and
Prithviraj Banerjee An algebraic array shape inference
system for MATLAB\reg . . . . . . . . . 848--907
Tim Brecht and
Eshrat Arjomandi and
Chang Li and
Hang Pham Controlling garbage collection and heap
growth to reduce the execution time of
Java applications . . . . . . . . . . . 908--941
Seon Wook Kim and
Chong-Liang Ooi and
Rudolf Eigenmann and
Babak Falsafi and
T. N. Vijaykumar Exploiting reference idempotency to
reduce speculative storage overflow . . 942--965
Rajeev Joshi and
Greg Nelson and
Yunhong Zhou Denali: a practical algorithm for
generating optimal code . . . . . . . . 967--989
Umut A. Acar and
Guy E. Blelloch and
Robert Harper Adaptive functional programming . . . . 990--1034
Jeffrey S. Foster and
Robert Johnson and
John Kodumal and
Alex Aiken Flow-insensitive type qualifiers . . . . 1035--1087
Mangala Gowri Nanda and
S. Ramesh Interprocedural slicing of multithreaded
programs with applications to Java . . . 1088--1144
Daniel J. Rosenkrantz and
Lenore R. Mullin and
Harry B. Hunt III On minimizing materializations of
array-valued temporaries . . . . . . . . 1145--1177
Vincent Simonet and
François Pottier A constraint-based approach to guarded
algebraic data types . . . . . . . . . . 1:1--1:56
Stephen M. Blackburn and
Matthew Hertz and
Kathryn S. Mckinley and
J. Eliot B. Moss and
Ting Yang Profile-based pretenuring . . . . . . . 2:1--2:57
Milenko Drini\'c and
Darko Kirovski and
Hoi Vo PPMexe: Program compression . . . . . . 3:1--3:31
Tomoyuki Higuchi and
Atsushi Ohori A static type system for JVM access
control . . . . . . . . . . . . . . . . 4:1--4:42
Amir M. Ben-Amram and
Chin Soon Lee Program termination analysis in
polynomial time . . . . . . . . . . . . 5:1--5:37
Patrick Eugster Type-based publish/subscribe: Concepts
and experiences . . . . . . . . . . . . 6:1--6:50
Martin Ward and
Hussein Zedan Slicing as a program transformation . . 7:1--7:53
Olivier Tardieu A deterministic logical semantics for
pure Esterel . . . . . . . . . . . . . . 8:1--8:26
Xiaotong Zhuang and
Santosh Pande Allocating architected registers through
differential encoding . . . . . . . . . 9:1--9:46
Maurice Bruynooghe and
Michael Codish and
John P. Gallagher and
Samir Genaim and
Wim Vanhoof Termination analysis of logic programs
through combination of type-based norms 10:1--10:44
Martin Hirzel and
Daniel Von Dincklage and
Amer Diwan and
Michael Hind Fast online pointer analysis . . . . . . 11:1--11:55
Jaydeep Marathe and
Frank Mueller and
Tushar Mohan and
Sally A. Mckee and
Bronis R. De Supinski and
Andy Yoo METRIC: Memory tracing via dynamic
binary rewriting to identify cache
inefficiencies . . . . . . . . . . . . . 12:1--12:36
D. Ancona and
C. Anderson and
F. Damiani and
S. Drossopoulou and
P. Giannini and
E. Zucca A provenly correct translation of Fickle
into Java . . . . . . . . . . . . . . . 13:1--13:67
Martín Abadi and
Jens Palsberg Editorial . . . . . . . . . . . . . . . 14:1--14:1
Andreas Podelski and
Andrey Rybalchenko Transition predicate abstraction and
fair termination . . . . . . . . . . . . 15:1--15:31
Yichen Xie and
Alex Aiken Saturn: a scalable framework for error
detection using Boolean satisfiability 16:1--16:43
J. Nathan Foster and
Michael B. Greenwald and
Jonathan T. Moore and
Benjamin C. Pierce and
Alan Schmitt Combinators for bidirectional tree
transformations: a linguistic approach
to the view-update problem . . . . . . . 17:1--17:65
Han B. Lee and
Amer Diwan and
J. Eliot B. Moss Design, implementation, and evaluation
of a compilation server . . . . . . . . 18:1--18:40
Bjorn De Sutter and
Ludo Van Put and
Koen De Bosschere A practical interprocedural dominance
algorithm . . . . . . . . . . . . . . . 19:1--19:44
Harel Paz and
David F. Bacon and
Elliot K. Kolodner and
Erez Petrank and
V. T. Rajan An efficient on-the-fly cycle collection 20:1--20:43
Anders Mòller and
Mads Òsterby Olesen and
Michael I. Schwartzbach Static validation of XSL transformations 21:1--21:47
Gareth Stoyle and
Michael Hicks and
Gavin Bierman and
Peter Sewell and
Iulian Neamtiu \em Mutatis Mutandis: Safe and
predictable dynamic software updating 22:1--22:70
Mooly Sagiv Introduction to special ESOP'05 issue 23:1--23:2
Bodil Biering and
Lars Birkedal and
Noah Torp-Smith BI-hyperdoctrines, higher-order
separation logic, and abstraction . . . 24:1--24:35
Cédric Fournet and
Andrew D. Gordon and
Sergio Maffeis A type discipline for authorization
policies . . . . . . . . . . . . . . . . 25:1--25:37
Xavier Rival and
Laurent Mauborgne The trace partitioning abstract domain 26:1--26:51
Venkatesh Prasad Ranganath and
Torben Amtoft and
Anindya Banerjee and
John Hatcliff and
Matthew B. Dwyer A new foundation for control dependence
and slicing for modern program
structures . . . . . . . . . . . . . . . 27:1--27:43
Ajay Chander and
David Espinosa and
Nayeem Islam and
Peter Lee and
George C. Necula Enforcing resource bounds via static
verification of dynamic checks . . . . . 28:1--28:18
Markus Müller-Olm and
Helmut Seidl Analysis of modular arithmetic . . . . . 29:1--29:27
Kathryn S. McKinley and
Keshav Pingali Editorial: a changing of the guard . . . 30:1--30:2
Kohei Honda and
Nobuko Yoshida A uniform type structure for secure
information flow . . . . . . . . . . . . 31:1--31:100
Christian Grothoff and
Jens Palsberg and
Jan Vitek Encapsulating objects with confined
types . . . . . . . . . . . . . . . . . 32:1--32:41
Thomas A. Henzinger and
Christoph M. Kirsch The embedded machine: Predictable,
portable real-time code . . . . . . . . 33:1--33:29
William Thies and
Frédéric Vivien and
Saman Amarasinghe A step towards unifying schedule and
storage optimization . . . . . . . . . . 34:1--34:45
Christian S. Collberg and
Clark Thomborson and
Gregg M. Townsend Dynamic graph-based software
fingerprinting . . . . . . . . . . . . . 35:1--35:67
Atsushi Ohori A proof theory for machine code . . . . 36:1--36:35
Kevin Casey and
M. Anton Ertl and
David Gregg Optimizing indirect branch prediction
accuracy in virtual machine interpreters 37:1--37:36
Bageshri Karkare and
Uday P. Khedker An improved bound for call strings based
interprocedural analysis of bit vector
frameworks . . . . . . . . . . . . . . . 38:1--38:13
Sunae Seo and
Hongseok Yang and
Kwangkeun Yi and
Taisook Han Goal-directed weakening of abstract
interpretation results . . . . . . . . . 39:1--39:39
Uday P. Khedker and
Amitabha Sanyal and
Amey Karkare Heap reference analysis using access
graphs . . . . . . . . . . . . . . . . . 1:1--1:41
Peng Zhao and
Shimin Cui and
Yaoqing Gao and
Raúl Silvera and
José Nelson Amaral \em Forma: a framework for safe
automatic array reshaping . . . . . . . 2:1--2:30
David Binkley and
Mark Harman and
Jens Krinke Empirical study of optimization
techniques for massive slicing . . . . . 3:1--3:33
David J. Pearce and
Paul H. J. Kelly and
Chris Hankin Efficient field-sensitive pointer
analysis of C . . . . . . . . . . . . . 4:1--4:42
Joseph (Yossi) Gil and
Yoav Zibin Efficient dynamic dispatching with type
slicing . . . . . . . . . . . . . . . . 5:1--5:53
Stephen Tse and
Steve Zdancewic Run-time principals in information-flow
type systems . . . . . . . . . . . . . . 6:1--6:42
Barak A. Pearlmutter and
Jeffrey Mark Siskind Reverse-mode AD in a functional
framework: Lambda the ultimate
backpropagator . . . . . . . . . . . . . 7:1--7:36
Westley Weimer and
George C. Necula Exceptional situations and program
reliability . . . . . . . . . . . . . . 8:1--8:51
Daniel E. Cooke and
J. Nelson Rushton and
Brad Nemanich and
Robert G. Watson and
Per Andersen Normalize, transpose, and distribute: an
automatic approach for handling
nonscalars . . . . . . . . . . . . . . . 9:1--9:49
Tao Wang and
Abhik Roychoudhury Dynamic slicing on Java bytecode traces 10:1--10:49
Luigi Liquori and
Arnaud Spiwack FeatherTrait: a modest extension of
Featherweight Java . . . . . . . . . . . 11:1--11:32
David Monniaux The pitfalls of verifying floating-point
computations . . . . . . . . . . . . . . 12:1--12:41
N. Rinetzky and
G. Ramalingam and
M. Sagiv and
E. Yahav On the complexity of
partially-flow-sensitive alias analysis 13:1--13:28
Daniel S. Dantas and
David Walker and
Geoffrey Washburn and
Stephanie Weirich AspectML: a polymorphic aspect-oriented
functional programming language . . . . 14:1--14:60
Tachio Terauchi and
Alex Aiken Witnessing side effects . . . . . . . . 15:1--15:42
Amir M. Ben-Amram Size-change termination with difference
constraints . . . . . . . . . . . . . . 16:1--16:31
Zhelong Pan and
Rudolf Eigenmann PEAK --- a fast and effective
performance tuning system via compiler
optimization orchestration . . . . . . . 17:1--17:43
Michael Furr and
Jeffrey S. Foster Checking type safety of foreign function
calls . . . . . . . . . . . . . . . . . 18:1--18:63
Ond\vrej Lhoták and
Laurie Hendren Relations as an abstraction for
BDD-based program analysis . . . . . . . 19:1--19:63
Cormac Flanagan and
Stephen N. Freund and
Marina Lifshin and
Shaz Qadeer Types for atomicity: Static checking and
inference for Java . . . . . . . . . . . 20:1--20:52
Andreas Gal and
Christian W. Probst and
Michael Franz Java bytecode verification via static
single assignment form . . . . . . . . . 21:1--21:21
Sapan Bhatia and
Charles Consel and
Calton Pu Remote specialization for efficient
embedded operating systems . . . . . . . 22:1--22:32
Hongbo Rong and
Alban Douillet and
Guang R. Gao Register allocation for software
pipelined multidimensional loops . . . . 23:1--23:68
Noah Torp-Smith and
Lars Birkedal and
John C. Reynolds Local reasoning about a copying garbage
collector . . . . . . . . . . . . . . . 24:1--24:58
Mila Dalla Preda and
Mihai Christodorescu and
Somesh Jha and
Saumya Debray A semantics-based approach to malware
detection . . . . . . . . . . . . . . . 25:1--25:54
James Cheney and
Christian Urban Nominal logic programming . . . . . . . 26:1--26:47
Tachio Terauchi and
Alex Aiken A capability calculus for concurrency
and determinism . . . . . . . . . . . . 27:1--27:30
Joseph (Yossi) Gil and
William Pugh and
Grant E. Weddell and
Yoav Zibin Two-dimensional bidirectional object
layout . . . . . . . . . . . . . . . . . 28:1--28:38
Mayur Naik and
Jens Palsberg A type system equivalent to a model
checker . . . . . . . . . . . . . . . . 29:1--29:24
Karthikeyan Bhargavan and
Cédric Fournet and
Andrew D. Gordon Verifying policy-based web services
security . . . . . . . . . . . . . . . . 30:1--30:59
Laurence Tratt Domain specific language implementation
via compile-time meta-programming . . . 31:1--31:40
Manuel Arenaz and
Juan Touriño and
Ramon Doallo XARK: an extensible framework for
automatic recognition of computational
kernels . . . . . . . . . . . . . . . . 32:1--32:56
Roland Ducournau Perfect hashing as an almost perfect
subtype test . . . . . . . . . . . . . . 33:1--33:56
Joseph M. Morris and
Malcolm Tyrrell Dually nondeterministic functions . . . 34:1--34:34
Bart Jacobs and
Frank Piessens and
Jan Smans and
K. Rustan M. Leino and
Wolfram Schulte A programming model for concurrent
object-oriented programs . . . . . . . . 1:1--1:48
Christian Schulte and
Peter J. Stuckey Efficient constraint propagation engines 2:1--2:43
C. Bernardeschi and
N. De Francesco and
G. Lettieri and
L. Martini and
P. Masci Decomposing bytecode verification by
abstract interpretation . . . . . . . . 3:1--3:63
Sungwoo Park and
Frank Pfenning and
Sebastian Thrun A probabilistic language based on
sampling functions . . . . . . . . . . . 4:1--4:46
Karthikeyan Bhargavan and
Cédric Fournet and
Andrew D. Gordon and
Stephen Tse Verified interoperable implementations
of security protocols . . . . . . . . . 5:1--5:57
Ana Lúcia De Moura and
Roberto Ierusalimschy Revisiting coroutines . . . . . . . . . 6:1--6:31
Todd Millstein and
Christopher Frost and
Jason Ryder and
Alessandro Warth Expressive and modular predicate
dispatch for Java . . . . . . . . . . . 7:1--7:54
Jon Sneyers and
Tom Schrijvers and
Bart Demoen The computational power and complexity
of constraint handling rules . . . . . . 8:1--8:42
Christian Schulte and
Peter J. Stuckey Erratum to: Efficient constraint
propagation engines . . . . . . . . . . 1--1
Steve MacDonald and
Kai Tan and
Jonathan Schaeffer and
Duane Szafron Deferring design pattern decisions and
automating structural pattern changes
using a design-pattern-based programming
system . . . . . . . . . . . . . . . . . 9:1--9:49
Chin Soon Lee Ranking functions for size-change
termination . . . . . . . . . . . . . . 10:1--10:42
Peter W. O'Hearn and
Hongseok Yang and
John C. Reynolds Separation and information hiding . . . 11:1--11:50
Jacob Matthews and
Robert Bruce Findler Operational semantics for multi-language
programs . . . . . . . . . . . . . . . . 12:1--12:44
Zena M. Ariola and
Aaron Bohannon and
Amr Sabry Sequent calculi and abstract machines 13:1--13:48
Sara Kalvala and
Richard Warburton and
David Lacey Program transformations using temporal
logic side conditions . . . . . . . . . 14:1--14:48
Davide Sangiorgi On the origins of bisimulation and
coinduction . . . . . . . . . . . . . . 15:1--15:41
Joseph M. Morris and
Alexander Bunkenburg and
Malcolm Tyrrell Term transformers: a new approach to
state . . . . . . . . . . . . . . . . . 16:1--16:42
Keshav Pingali and
Kathryn McKinley Remembrances of things past . . . . . . 17:1--17:2
Efe Yardimci and
Michael Franz Mostly static program partitioning of
binary executables . . . . . . . . . . . 17:1--17:46
Gilles Barthe and
Benjamin Grégoire and
César Kunz and
Tamara Rezk Certificate translation for optimizing
compilers . . . . . . . . . . . . . . . 18:1--18:45
Giuseppe Castagna and
Nils Gesbert and
Luca Padovani A theory of contracts for Web services 19:1--19:61
Yutao Zhong and
Xipeng Shen and
Chen Ding Program locality analysis using reuse
distance . . . . . . . . . . . . . . . . 20:1--20:39
Yanhong A. Liu and
Scott D. Stoller From datalog rules to efficient programs
with time and space guarantees . . . . . 21:1--21:38
Shlomi Dolev and
Yinnon Haviv and
Mooly Sagiv Self-stabilization preserving compiler 22:1--22:22
Massimo Bartoletti and
Pierpaolo Degano and
Gian-Luigi Ferrari and
Roberto Zunino Local policies for resource usage
analysis . . . . . . . . . . . . . . . . 23:1--23:43
Mark Harman and
David Binkley and
Keith Gallagher and
Nicolas Gold and
Jens Krinke Dependence clusters in source code . . . 1:1--1:33
Haruo Hosoya and
Alain Frisch and
Giuseppe Castagna Parametric polymorphism for XML . . . . 2:1--2:56
Umut A. Acar and
Guy E. Blelloch and
Matthias Blume and
Robert Harper and
Kanat Tangwongsan An experimental analysis of
self-adjusting computation . . . . . . . 3:1--3:53
Shane Markstrum and
Daniel Marino and
Matthew Esquivel and
Todd Millstein and
Chris Andreae and
James Noble JavaCOP: Declarative pluggable types for
Java . . . . . . . . . . . . . . . . . . 4:1--4:37
Bertrand Jeannet and
Alexey Loginov and
Thomas Reps and
Mooly Sagiv A relational approach to interprocedural
shape analysis . . . . . . . . . . . . . 5:1--5:52
Kenneth Knowles and
Cormac Flanagan Hybrid type checking . . . . . . . . . . 6:1--6:34
Amal Ahmed and
Andrew W. Appel and
Christopher D. Richards and
Kedar N. Swadi and
Gang Tan and
Daniel C. Wang Semantic foundations for typed assembly
languages . . . . . . . . . . . . . . . 7:1--7:67
Fausto Spoto and
Fred Mesnard and
Étienne Payet A termination analyzer for Java bytecode
based on path-length . . . . . . . . . . 8:1--8:70
Rob V. Van Nieuwpoort and
Gosia Wrzesi\'nska and
Ceriel J. H. Jacobs and
Henri E. Bal Satin: a high-level and efficient grid
programming model . . . . . . . . . . . 9:1--9:39
Kathryn S. Mckinley and
Keshav Pingali La dolce vita at TOPLAS . . . . . . . . 10:1--10:6
Xiaotong Zhuang and
Santosh Pande An optimization framework for embedded
processors with auto-addressing mode . . 11:1--11:41
Peter Sewell and
Pawe\l T. Wojciechowski and
Asis Unyapoth Nomadic pict: Programming languages,
communication infrastructure overlays,
and semantics for mobile computation . . 12:1--12:63
Vivy Suhendra and
Abhik Roychoudhury and
Tulika Mitra Scratchpad allocation for concurrent
embedded software . . . . . . . . . . . 13:1--13:47
Peter H. Welch and
Jan B. Pedersen Santa Claus: Formal analysis of a
process-oriented solution . . . . . . . 14:1--14:37
Yuqiang Huang and
Bruce R. Childers and
Mary Lou Soffa Detecting bugs in register allocation 15:1--15:36
Naoki Kobayashi and
Davide Sangiorgi A hybrid type system for lock-freedom of
mobile processes . . . . . . . . . . . . 16:1--16:49
Dennis Jeffrey and
Vijay Nagarajan and
Rajiv Gupta and
Neelam Gupta Execution suppression: an automated
iterative technique for locating memory
errors . . . . . . . . . . . . . . . . . 17:1--17:36
Eran Yahav and
Mooly Sagiv Verifying safety properties of
concurrent heap-manipulating programs 18:1--18:50
Sven Apel and
Delesley Hutchins A calculus for uniform feature
composition . . . . . . . . . . . . . . 19:1--19:33
Kathryn S. Mckinley and
Keshav Pingali La prossima vita at TOPLAS . . . . . . . 20:1--20:1
Salvatore Ruggieri and
Fred Mesnard Typing linear constraints . . . . . . . 21:1--21:42
John Tang Boyland Semantics of fractional permissions with
nesting . . . . . . . . . . . . . . . . 22:1--22:33
Gogul Balakrishnan and
Thomas Reps WYSINWYX: What you see is not what you
eXecute . . . . . . . . . . . . . . . . 23:1--23:84
Thomas Reps and
Mooly Sagiv and
Alexey Loginov Finite differencing of logical formulas
for static analysis . . . . . . . . . . 24:1--24:55
Jens Palsberg Editorial . . . . . . . . . . . . . . . 1:1--1:1
Martín Abadi and
Andrew Birrell and
Tim Harris and
Michael Isard Semantics of transactional memory and
automatic mutual exclusion . . . . . . . 2:1--2:50
Polyvios Pratikakis and
Jeffrey S. Foster and
Michael Hicks LOCKSMITH: Practical static race
detection for C . . . . . . . . . . . . 3:1--3:55
John Derrick and
Gerhard Schellhorn and
Heike Wehrheim Mechanically verified proof obligations
for linearizability . . . . . . . . . . 4:1--4:43
Davide Sangiorgi and
Naoki Kobayashi and
Eijiro Sumii Environmental bisimulations for
higher-order languages . . . . . . . . . 5:1--5:69
Shan Shan Huang and
Yannis Smaragdakis Morphing: Structurally shaping a class
by reflecting on others . . . . . . . . 6:1--6:44
Jürgen Giesl and
Matthias Raffelsieper and
Peter Schneider-Kamp and
Stephan Swiderski and
René Thiemann Automated termination proofs for Haskell
by term rewriting . . . . . . . . . . . 7:1--7:39
Jesper Bengtson and
Karthikeyan Bhargavan and
Cédric Fournet and
Andrew D. Gordon and
Sergio Maffeis Refinement types for secure
implementations . . . . . . . . . . . . 8:1--8:45
Frank Tip and
Robert M. Fuhrer and
Adam Kie\.zun and
Michael D. Ernst and
Ittai Balaban and
Bjorn De Sutter Refactoring using type constraints . . . 9:1--9:47
Utpal Banerjee Mathematical foundation of trace
scheduling . . . . . . . . . . . . . . . 10:1--10:24
Thomas Martin Gawlitza and
Helmut Seidl Solving systems of rational equations
through strategy iteration . . . . . . . 11:1--11:48
Stefan Wehr and
Peter Thiemann JavaGI: The Interaction of Type Classes
with Interfaces and Inheritance . . . . 12:1--12:83
Gilles Barthe and
César Kunz An Abstract Model of Certificate
Translation . . . . . . . . . . . . . . 13:1--13:46
Stavros Tripakis and
Ben Lickly and
Thomas A. Henzinger and
Edward A. Lee A Theory of Synchronous Relational
Interfaces . . . . . . . . . . . . . . . 14:1--14:41
Rajeev Alur and
Swarat Chaudhuri and
P. Madhusudan Software model checking using languages
of nested trees . . . . . . . . . . . . 15:1--15:45
Christos Dimoulas and
Matthias Felleisen On contract satisfaction in a
higher-order world . . . . . . . . . . . 16:1--16:29
Bhargav S. Gulavani and
Supratik Chakraborty and
G. Ramalingam and
Aditya V. Nori Bottom-up shape analysis using LISF . . 17:1--17:41
Jens Palsberg Editorial note . . . . . . . . . . . . . 18:1--18:1
Mingsheng Ying Floyd--Hoare logic for quantum programs 19:1--19:49
Werner Dietl and
Sophia Drossopoulou and
Peter Müller Separating ownership topology and
encapsulation with generic universe
types . . . . . . . . . . . . . . . . . 20:1--20:62
Andrea Flexeder and
Markus Müller-olm and
Michael Petter and
Helmut Seidl Fast interprocedural linear two-variable
equalities . . . . . . . . . . . . . . . 21:1--21:33
Jens Palsberg Editorial . . . . . . . . . . . . . . . 1:1--1:1
Jan Smans and
Bart Jacobs and
Frank Piessens Implicit dynamic frames . . . . . . . . 2:1--2:58
Lakshminarayanan Renganarayanan and
Daegon Kim and
Michelle Mills Strout and
Sanjay Rajopadhye Parameterized loop tiling . . . . . . . 3:1--3:41
Julian Dolby and
Christian Hammer and
Daniel Marino and
Frank Tip and
Mandana Vaziri and
Jan Vitek A data-centric approach to
synchronization . . . . . . . . . . . . 4:1--4:48
Xing Wu and
Frank Mueller ScalaExtrap: Trace-based communication
extrapolation for SPMD programs . . . . 5:1--5:29
Pierre Ganty and
Rupak Majumdar Algorithmic verification of asynchronous
programs . . . . . . . . . . . . . . . . 6:1--6:48
Eric Bodden and
Patrick Lam and
Laurie Hendren Partially Evaluating Finite-State
Runtime Monitors Ahead of Time . . . . . 7:1--7:52
Marco Carbone and
Kohei Honda and
Nobuko Yoshida Structured Communication-Centered
Programming for Web Services . . . . . . 8:1--8:78
Pramod G. Joisha and
Robert S. Schreiber and
Prithviraj Banerjee and
Hans-J. Boehm and
Dhruva R. Chakrabarti On a Technique for Transparently
Empowering Classical Compiler
Optimizations on Multithreaded Code . . 9:1--9:42
Gérard Boudol and
Zhengqin Luo and
Tamara Rezk and
Manuel Serrano Reasoning about Web Applications: An
Operational Semantics for HOP . . . . . 10:1--10:40
Sven Verdoolaege and
Gerda Janssens and
Maurice Bruynooghe Equivalence checking of static affine
programs using widening to handle
recurrences . . . . . . . . . . . . . . 11:1--11:35
Bruno De Fraine and
Erik Ernst and
Mario Südholt Essential AOP: The $A$ calculus . . . . 12:1--12:43
Anna Bendersky and
Erez Petrank Space overhead bounds for dynamic memory
management with partial compaction . . . 13:1--13:43
Jan Hoffmann and
Klaus Aehlig and
Martin Hofmann Multivariate amortized resource analysis 14:1--14:62
Maartje de Jonge and
Lennart C. L. Kats and
Eelco Visser and
Emma Söderberg Natural and Flexible Error Recovery for
Generated Modular Language Environments 15:1--15:50
Amir M. Ben-Amram and
Samir Genaim and
Abu Naser Masud On the Termination of Integer Loops . . 16:1--16:24
Yuan Feng and
Runyao Duan and
Mingsheng Ying Bisimulation for Quantum Processes . . . 17:1--17:43
Jens Palsberg Editorial . . . . . . . . . . . . . . . 1:1--1:??
Andreas Rossberg and
Derek Dreyer Mixin' Up the ML Module System . . . . . 2:1--2:??
V. Krishna Nandivada and
Jun Shirako and
Jisheng Zhao and
Vivek Sarkar A Transformation Framework for
Optimizing Task-Parallel Programs . . . 3:1--3:??
Junghee Lim and
Thomas Reps TSL: a System for Generating Abstract
Interpreters and its Application to
Machine-Code Analysis . . . . . . . . . 4:1--4:??
Stefan Staiger-Stöhr Practical Integrated Analysis of
Pointers, Dataflow and Control Flow . . 5:1--5:??
Aleksandar Nanevski and
Anindya Banerjee and
Deepak Garg Dependent Type Theory for Verification
of Information Flow and Access Control
Policies . . . . . . . . . . . . . . . . 6:1--6:??
David Binkley and
Nicolas Gold and
Mark Harman and
Syed Islam and
Jens Krinke and
Zheng Li Efficient Identification of Linchpin
Vertices in Dependence Clusters . . . . 7:1--7:??
Matko Botincan and
Mike Dodds and
Suresh Jagannathan Proof-Directed Parallelization Synthesis
by Separation Logic . . . . . . . . . . 8:1--8:??
Gilles Barthe and
Boris Köpf and
Federico Olmedo and
Santiago Zanella-Béguelin Probabilistic Relational Reasoning for
Differential Privacy . . . . . . . . . . 9:1--9:49
Ahmed Bouajjani and
Michael Emmi Analysis of Recursively Parallel
Programs . . . . . . . . . . . . . . . . 10:1--10:49
T. Stephen Strickland and
Christos Dimoulas and
Asumu Takikawa and
Matthias Felleisen Contracts for First-Class Classes . . . 11:1--11:58
Andreas Lochbihler Making the Java memory model safe . . . 12:1--12:??
Diogo Sampaio and
Rafael Martins de Souza and
Sylvain Collange and
Fernando Magno Quintão Pereira Divergence analysis . . . . . . . . . . 13:1--13:??
Durica Nikoli\'c and
Fausto Spoto Reachability analysis of program
variables . . . . . . . . . . . . . . . 14:1--14:??
Sheng Chen and
Martin Erwig and
Eric Walkingshaw Extending Type Inference to Variational
Programs . . . . . . . . . . . . . . . . 1:1--1:??
Sven Stork and
Karl Naden and
Joshua Sunshine and
Manuel Mohr and
Alcides Fonseca and
Paulo Marques and
Jonathan Aldrich Æminium: a Permission-Based
Concurrent-by-Default Programming
Language Approach . . . . . . . . . . . 2:1--2:??
Hongjin Liang and
Xinyu Feng and
Ming Fu Rely-Guarantee-Based Simulation for
Compositional Verification of Concurrent
Program Transformations . . . . . . . . 3:1--3:??
Gilles Barthe and
Delphine Demange and
David Pichardie Formal Verification of an SSA-Based
Middle-End for CompCert . . . . . . . . 4:1--4:??
Min Aung and
Susan Horwitz and
Rich Joiner and
Thomas Reps Specialization Slicing . . . . . . . . . 5:1--5:??
Suresh Jagannathan and
Vincent Laporte and
Gustavo Petri and
David Pichardie and
Jan Vitek Atomicity Refinement for Verified
Compilation . . . . . . . . . . . . . . 6:1--6:??
Jade Alglave and
Luc Maranget and
Michael Tautschnig Herding Cats: Modelling, Simulation,
Testing, and Data Mining for Weak Memory 7:1--7:??
Hakjoo Oh and
Kihong Heo and
Wonchan Lee and
Woosuk Lee and
Daejun Park and
Jeehoon Kang and
Kwangkeun Yi Global Sparse Analysis Framework . . . . 8:1--8:??
Javier Esparza and
Pierre Ganty and
Tomás Poch Pattern-Based Verification for
Multithreaded Programs . . . . . . . . . 9:1--9:??
Alexandros Tzannes and
George C. Caragea and
Uzi Vishkin and
Rajeev Barua Lazy Scheduling: a Runtime Adaptive
Scheduler for Declarative Parallelism 10:1--10:??
Matt Elder and
Junghee Lim and
Tushar Sharma and
Tycho Andersen and
Thomas Reps Abstract Domains of Affine Relations . . 11:1--11:??
Ronald Garcia and
Éric Tanter and
Roger Wolff and
Jonathan Aldrich Foundations of Typestate-Oriented
Programming . . . . . . . . . . . . . . 12:1--12:??
Christopher M. Hayden and
Karla Saur and
Edward K. Smith and
Michael Hicks and
Jeffrey S. Foster Kitsune: Efficient, General-Purpose
Dynamic Software Updating for C . . . . 13:1--13:??
Alexander Kaiser and
Daniel Kroening and
Thomas Wahl A Widening Approach to Multithreaded
Program Verification . . . . . . . . . . 14:1--14:??
Graeme Gange and
Jorge A. Navas and
Peter Schachte and
Harald Sòndergaard and
Peter J. Stuckey Interval Analysis and Machine
Arithmetic: Why Signedness Ignorance Is
Bliss . . . . . . . . . . . . . . . . . 1:1--1:??
Jens Palsberg Editorial . . . . . . . . . . . . . . . 1:1--1:??
Tony Nowatzki and
Michael Sartin-Tarm and
Lorenzo De Carli and
Karthikeyan Sankaralingam and
Cristian Estan and
Behnam Robatmili A Scheduling Framework for Spatial
Architectures Across Multiple
Constraint-Solving Theories . . . . . . 2:1--2:??
Camil Demetrescu and
Irene Finocchi and
Andrea Ribichini Reactive Imperative Programming with
Dataflow Constraints . . . . . . . . . . 3:1--3:??
Donald E. Porter and
Michael D. Bond and
Indrajit Roy and
Kathryn S. Mckinley and
Emmett Witchel Practical Fine-Grained Information Flow
Control Using Laminar . . . . . . . . . 4:1--4:??
Michael Frechtling and
Philip H. W. Leong MCALIB: Measuring Sensitivity to
Rounding Error with Monte Carlo
Programming . . . . . . . . . . . . . . 5:1--5:??
Marco Patrignani and
Pieter Agten and
Raoul Strackx and
Bart Jacobs and
Dave Clarke and
Frank Piessens Secure Compilation to Protected Module
Architectures . . . . . . . . . . . . . 6:1--6:??
Andrew W. Appel Verification of a Cryptographic
Primitive: SHA-256 . . . . . . . . . . . 7:1--7:??
Baris Kasikci and
Cristian Zamfir and
George Candea Automated Classification of Data Races
Under Both Strong and Weak Memory Models 8:1--8:??
Farn Wang and
Sven Schewe and
Chung-Hao Huang An Extension of ATL with Strategy
Interaction . . . . . . . . . . . . . . 9:1--9:??
Adam Betts and
Nathan Chong and
Alastair F. Donaldson and
Jeroen Ketema and
Shaz Qadeer and
Paul Thomson and
John Wickerson The Design and Implementation of a
Verification Technique for GPU Kernels 10:1--10:??
Michele Bugliesi and
Stefano Calzavara and
Fabienne Eigner and
Matteo Maffei Affine Refinement Types for Secure
Distributed Programming . . . . . . . . 11:1--11:??
Tobias Grosser and
Sven Verdoolaege and
Albert Cohen Polyhedral AST Generation Is More Than
Scanning Polyhedra . . . . . . . . . . . 12:1--12:??
Gary T. Leavens and
David A. Naumann Behavioral Subtyping, Specification
Inheritance, and Modular Reasoning . . . 13:1--13:??
Loris D'antoni and
Margus Veanes and
Benjamin Livshits and
David Molnar Fast: a Transducer-Based Language for
Tree Manipulation . . . . . . . . . . . 1:1--1:??
Dariusz Biernacki and
Olivier Danvy and
Kevin Millikin A Dynamic Continuation-Passing Style for
Dynamic Delimited Continuations . . . . 2:1--2:??
Nils Gesbert and
Pierre Genev\`es and
Nabil Laya\"\ida A Logical Approach to Deciding Semantic
Subtyping . . . . . . . . . . . . . . . 3:1--3:??
Mike Dodds and
Suresh Jagannathan and
Matthew J. Parkinson and
Kasper Svendsen and
Lars Birkedal Verifying Custom Synchronization
Constructs Using Higher-Order Separation
Logic . . . . . . . . . . . . . . . . . 4:1--4:??
Paraskevas Yiapanis and
Gavin Brown and
Mikel Luján Compiler-Driven Software Speculation for
Thread-Level Parallelism . . . . . . . . 5:1--5:??
Hakjoo Oh and
Wonchan Lee and
Kihong Heo and
Hongseok Yang and
Kwangkeun Yi Selective X-Sensitive Analysis Guided by
Impact Pre-Analysis . . . . . . . . . . 6:1--6:??
Stefano Dissegna and
Francesco Logozzo and
Francesco Ranzato An Abstract Interpretation-Based Model
of Tracing Just-in-Time Compilation . . 7:1--7:??
Sukyoung Ryu ThisType for Object-Oriented Languages:
From Theory to Practice . . . . . . . . 8:1--8:??
Gregor Wagner and
Per Larsen and
Stefan Brunthaler and
Michael Franz Thinking Inside the Box:
Compartmentalized Garbage Collection . . 9:1--9:??
Brian Norris and
Brian Demsky A Practical Approach for Model Checking
C/C++11 Code . . . . . . . . . . . . . . 10:1--10:??
Somashekaracharya G. Bhaskaracharya and
Uday Bondhugula and
Albert Cohen Automatic Storage Optimization for
Arrays . . . . . . . . . . . . . . . . . 11:1--11:??
Uday Bondhugula and
Aravind Acharya and
Albert Cohen The Pluto+ Algorithm: a Practical
Approach for Parallelization and
Locality Optimization of Affine Loop
Nests . . . . . . . . . . . . . . . . . 12:1--12:??
Marc Brockschmidt and
Fabian Emmes and
Stephan Falke and
Carsten Fuhs and
Jürgen Giesl Analyzing Runtime and Size Complexity of
Integer Programs . . . . . . . . . . . . 13:1--13:??
Thibaut Balabonski and
François Pottier and
Jonathan Protzenko The Design and Formalization of Mezzo, a
Permission-Based Programming Language 14:1--14:??
Stephen M. Blackburn and
Amer Diwan and
Matthias Hauswirth and
Peter F. Sweeney and
José Nelson Amaral and
Tim Brecht and
Lubomír Bulej and
Cliff Click and
Lieven Eeckhout and
Sebastian Fischmeister and
Daniel Frampton and
Laurie J. Hendren and
Michael Hind and
Antony L. Hosking and
Richard E. Jones and
Tomas Kalibera and
Nathan Keynes and
Nathaniel Nystrom and
Andreas Zeller The Truth, The Whole Truth, and Nothing
But the Truth: a Pragmatic Guide to
Assessing Empirical Evaluations . . . . 15:1--15:??
Daniel Marino and
Abhayendra Singh and
Todd Millstein and
Madanlal Musuvathi and
Satish Narayanasamy drf x: an Understandable, High
Performance, and Flexible Memory Model
for Concurrent Languages . . . . . . . . 16:1--16:??
Andrew Myers Foreword . . . . . . . . . . . . . . . . 1:1--1:??
Nachshon Cohen and
Erez Petrank Limitations of Partial Compaction:
Towards Practical Bounds . . . . . . . . 2:1--2:??
Taro Sekiyama and
Atsushi Igarashi and
Michael Greenberg Polymorphic Manifest Contracts, Revised
and Resolved . . . . . . . . . . . . . . 3:1--3:??
Jay Ligatti and
Jeremy Blackburn and
Michael Nachtigal On Subtyping-Relation Completeness, with
an Application to Iso-Recursive Types 4:1--4:??
Martin Hirzel and
Scott Schneider and
Bugra Gedik SPL: an Extensible Language for
Distributed Stream Processing . . . . . 5:1--5:??
Jade Alglave and
Daniel Kroening and
Vincent Nimal and
Daniel Poetzl Don't Sit on the Fence: a Static
Analysis Approach to Automatic Fence
Insertion . . . . . . . . . . . . . . . 6:1--6:??
Marie-Christine Jakobs and
Heike Wehrheim Programs from Proofs: a Framework for
the Safe Execution of Untrusted Software 7:1--7:??
Eva Darulova and
Viktor Kuncak Towards a Compiler for Reals . . . . . . 8:1--8:??
Thomas Reps and
Emma Turetsky and
Prathmesh Prabhu Newtonian Program Analysis via Tensor
Product . . . . . . . . . . . . . . . . 9:1--9:??
Thomas H. Austin and
Tommy Schmitz and
Cormac Flanagan Multiple Facets for Dynamic Information
Flow with Exceptions . . . . . . . . . . 10:1--10:??
Colin S. Gordon and
Michael D. Ernst and
Dan Grossman and
Matthew J. Parkinson Verifying Invariants of Lock-Free Data
Structures with Rely-Guarantee and
Refinement Types . . . . . . . . . . . . 11:1--11:??
Jacques-Henri Jourdan and
François Pottier A Simple, Possibly Correct LR Parser for
C11 . . . . . . . . . . . . . . . . . . 14:1--14:??
Vojt\uach Forejt and
Saurabh Joshi and
Daniel Kroening and
Ganesh Narayanaswamy and
Subodh Sharma Precise Predictive Analysis for
Discovering Communication Deadlocks in
MPI Programs . . . . . . . . . . . . . . 15:1--15:??
Woosuk Lee and
Wonchan Lee and
Dongok Kang and
Kihong Heo and
Hakjoo Oh and
Kwangkeun Yi Sound Non-Statistical Clustering of
Static Analysis Alarms . . . . . . . . . 16:1--16:??
Phil Trinder and
Natalia Chechina and
Nikolaos Papaspyrou and
Konstantinos Sagonas and
Simon Thompson and
Stephen Adams and
Stavros Aronis and
Robert Baker and
Eva Bihari and
Olivier Boudeville and
Francesco Cesarini and
Maurizio Di Stefano and
Sverker Eriksson and
Viktória Förd\Hos and
Amir Ghaffari and
Aggelos Giantsios and
Rickard Green and
Csaba Hoch and
David Klaftenegger and
Huiqing Li and
Kenneth Lundin and
Kenneth Mackenzie and
Katerina Roukounaki and
Yiannis Tsiouris and
Kjell Winblad Scaling Reliably: Improving the
Scalability of the Erlang Distributed
Actor Platform . . . . . . . . . . . . . 17:1--17:??
Danfeng Zhang and
Andrew C. Myers and
Dimitrios Vytiniotis and
Simon Peyton-Jones SHErrLoc: a Static Holistic Error
Locator . . . . . . . . . . . . . . . . 18:1--18:??
Hong-Yi Chen and
Cristina David and
Daniel Kroening and
Peter Schrammel and
Björn Wachter Bit-Precise Procedure-Modular
Termination Analysis . . . . . . . . . . 1:1--1:??
Friedrich Steimann Constraint-Based Refactoring . . . . . . 2:1--2:??
Jacob Lidman and
Sally A. Mckee Verifying Reliability Properties Using
the Hyperball Abstract Domain . . . . . 3:1--3:??
Federico Olmedo and
Friedrich Gretz and
Nils Jansen and
Benjamin Lucien Kaminski and
Joost-Pieter Katoen and
Annabelle Mciver Conditioning in Probabilistic
Programming . . . . . . . . . . . . . . 4:1--4:??
Cristina David and
Pascal Kesseli and
Daniel Kroening and
Matt Lewis Program Synthesis for Program Analysis 5:1--5:??
Anindya Banerjee and
David A. Naumann and
Mohammad Nikouei A Logical Analysis of Framing for
Specifications with Pure Method Calls 6:1--6:??
Krishnendu Chatterjee and
Hongfei Fu and
Petr Novotný and
Rouzbeh Hasheminezhad Algorithmic Analysis of Qualitative and
Quantitative Termination Problems for
Affine Probabilistic Programs . . . . . 7:1--7:??
Matthias Grimmer and
Roland Schatz and
Chris Seaton and
Thomas Würthinger and
Mikel Luján Cross-Language Interoperability in a
Multi-Language Runtime . . . . . . . . . 8:1--8:??
Krishnendu Chatterjee and
Rasmus Ibsen-Jensen and
Amir Kafshdar Goharshady and
Andreas Pavlogiannis Algorithms for Algebraic Path Properties
in Concurrent Systems of Constant
Treewidth Components . . . . . . . . . . 9:1--9:??
Spencer P. Florence and
Burke Fetscher and
Matthew Flatt and
William H. Temps and
Vincent St-Amour and
Tina Kiguradze and
Dennis P. West and
Charlotte Niznik and
Paul R. Yarnold and
Robert Bruce Findler and
Steven M. Belknap POP-PL: a Patient-Oriented Prescription
Programming Language . . . . . . . . . . 10:1--10:??
Sebastian Danicic and
Michael R. Laurence Static Backward Slicing of
Non-deterministic Programs and Systems 11:1--11:??
Andrew Myers Editor's Foreword to ``Static Backward
Slicing of Non-Deterministic Programs
and Systems'' . . . . . . . . . . . . . 11:1--11:??
Bart Jacobs and
Dragan Bosnacki and
Ruurd Kuiper Modular Termination Verification of
Single-Threaded and Multithreaded
Programs . . . . . . . . . . . . . . . . 12:1--12:??
Se-Won Kim and
Xavier Rival and
Sukyoung Ryu A Theoretical Foundation of Sensitivity
in an Abstract Interpretation Framework 13:1--13:??
Kihong Heo and
Hakjoo Oh and
Hongseok Yang and
Kwangkeun Yi Adaptive Static Analysis via Learning
with Bayesian Optimization . . . . . . . 14:1--14:??
Tomoharu Ugawa and
Carl G. Ritson and
Richard E. Jones Transactional Sapphire: Lessons in
High-Performance, On-the-fly Garbage
Collection . . . . . . . . . . . . . . . 15:1--15:??
Matías Toro and
Ronald Garcia and
Éric Tanter Type-Driven Gradual Security with
References . . . . . . . . . . . . . . . 16:1--16:??
Bernardo Toninho and
Nobuko Yoshida Interconnectability of Session-Based
Logical Processes . . . . . . . . . . . 17:1--17:??
Anonymous Corrigendum to ``Cross-Language
Interoperability in a Multi-Language
Runtime'', by Grimmer et al., ACM
Transactions on Programming Languages
and Systems (TOPLAS) Volume 40, Issue 2,
Article No. 8 . . . . . . . . . . . . . 18:1--18:??
Tiago Cogumbreiro and
Raymond Hu and
Francisco Martins and
Nobuko Yoshida Dynamic Deadlock Verification for
General Barrier Synchronisation . . . . 1:1--1:??
Alexey Solovyev and
Marek S. Baranowski and
Ian Briggs and
Charles Jacobsen and
Zvonimir Rakamari\'c and
Ganesh Gopalakrishnan Rigorous Estimation of Floating-Point
Round-Off Errors with Symbolic Taylor
Expansions . . . . . . . . . . . . . . . 2:1--2:??
Nicholas Jacek and
Meng-Chieh Chiu and
Benjamin M. Marlin and
J. Eliot B. Moss Optimal Choice of When to Garbage
Collect . . . . . . . . . . . . . . . . 3:1--3:??
Leif Andersen and
Vincent St-Amour and
Jan Vitek and
Matthias Felleisen Feature-Specific Profiling . . . . . . . 4:1--4:??
Rodolphe Lepigre and
Christophe Raffalli Practical Subtyping for Curry-Style
Languages . . . . . . . . . . . . . . . 5:1--5:??
Bozhen Liu and
Jeff Huang and
Lawrence Rauchwerger Rethinking Incremental and Parallel
Pointer Analysis . . . . . . . . . . . . 6:1--6:??
Andrew Myers Editorial . . . . . . . . . . . . . . . 7:1--7:??
Étienne Miquey A Classical Sequent Calculus with
Dependent Types . . . . . . . . . . . . 8:1--8:??
Luca Padovani Context-Free Session Type Inference . . 9:1--9:??
Ugo Dal Lago and
Charles Grellois Probabilistic Termination by Monadic
Affine Sized Typing . . . . . . . . . . 10:1--10:??
Conrad Cotton-Barratt and
Andrzej S. Murawski and
C.-H. Luke Ong ML, Visibly Pushdown Class Memory
Automata, and Extended Branching Vector
Addition Systems with States . . . . . . 11:1--11:??
Matthew Hague and
Anthony W. Lin and
Chih-Duo Hong CSS Minification via Constraint Solving 12:1--12:??
Minseok Jeon and
Sehun Jeong and
Sungdeok Cha and
Hakjoo Oh A Machine-Learning Algorithm with
Disjunctive Model for Data-Driven
Program Analysis . . . . . . . . . . . . 13:1--13:??
Leandro Facchinetti and
Zachary Palmer and
Scott Smith Higher-order Demand-driven Program
Analysis . . . . . . . . . . . . . . . . 14:1--14:??
David Grove and
Sara S. Hamouda and
Benjamin Herta and
Arun Iyengar and
Kiyokuni Kawachiya and
Josh Milthorpe and
Vijay Saraswat and
Avraham Shinnar and
Mikio Takeuchi and
Olivier Tardieu Failure Recovery in Resilient X10 . . . 15:1--15:??
Manas Thakur and
V. Krishna Nandivada PYE: a Framework for
Precise-Yet-Efficient Just-In-Time
Analyses for Java Programs . . . . . . . 16:1--16:??
Roberto Castañeda Lozano and
Mats Carlsson and
Gabriel Hjort Blindell and
Christian Schulte Combinatorial Register Allocation and
Instruction Scheduling . . . . . . . . . 17:1--17:??
Fausto Spoto and
Elisa Burato and
Michael D. Ernst and
Pietro Ferrara and
Alberto Lovato and
Damiano Macedonio and
Ciprian Spiridon Static Identification of Injection
Attacks in Java . . . . . . . . . . . . 18:1--18:??
Andrea Ros\`a and
Eduardo Rosales and
Walter Binder Analysis and Optimization of Task
Granularity on the Java Virtual Machine 19:1--19:??
Krishnendu Chatterjee and
Hongfei Fu and
Amir Kafshdar Goharshady Non-polynomial Worst-Case Analysis of
Recursive Programs . . . . . . . . . . . 20:1--20:??
Emery D. Berger and
Celeste Hollenbeck and
Petr Maj and
Olga Vitek and
Jan Vitek On the Impact of Programming Languages
on Code Quality: a Reproduction Study 21:1--21:??
Davide Sangiorgi and
Valeria Vignudelli Environmental Bisimulations for
Probabilistic Higher-order Languages . . 22:1--22:??
Krishnendu Chatterjee and
Amir Kafshdar Goharshady and
Prateesh Goyal and
Rasmus Ibsen-Jensen and
Andreas Pavlogiannis Faster Algorithms for Dynamic Algebraic
Queries in Basic RSMs with Constant
Treewidth . . . . . . . . . . . . . . . 23:1--23:??
Amal Ahmed Introduction to the Special Issue on
ESOP 2018 . . . . . . . . . . . . . . . 1--1
Ningning Xie and
Xuan Bi and
Bruno C. D. S. Oliveira and
Tom Schrijvers Consistent Subtyping for All . . . . . . 2:1--2:??
Marco Eilers and
Peter Müller and
Samuel Hitz Modular Product Programs . . . . . . . . 3:1--3:??
Alex Simpson and
Niels Voorneveld Behavioural Equivalence via Modalities
for Algebraic Effects . . . . . . . . . 4:1--4:??
Lau Skorstengaard and
Dominique Devriese and
Lars Birkedal Reasoning about a Machine with Local
Capabilities: Provably Safe Stack and
Return Pointer Management . . . . . . . 1--53
Torben Amtoft and
Anindya Banerjee A Theory of Slicing for Imperative
Probabilistic Programs . . . . . . . . . 6:1--6:71
David Zhao and
Pavle Suboti\'c and
Bernhard Scholz Debugging Large-scale Datalog: a
Scalable Provenance Evaluation Strategy 7:1--7:35
Pritam M. Gharat and
Uday P. Khedker and
Alan Mycroft Generalized Points-to Graphs: a Precise
and Scalable Abstraction for Points-to
Analysis . . . . . . . . . . . . . . . . 8:1--8:78
Praveen Narayanan and
Chung-chieh Shan Symbolic Disintegration with a Variety
of Base Measures . . . . . . . . . . . . 9:1--9:60
Yue Li and
Tian Tan and
Anders Mòller and
Yannis Smaragdakis A Principled Approach to Selective
Context Sensitivity for Pointer Analysis 10:1--10:40
Matías Toro and
Ronald Garcia and
Éric Tanter Corrigendum to ``Type-driven Gradual
Security with References,'' by Toro et
al., ACM Transactions on Programming
Languages and Systems (TOPLAS) Volume
\bf 40, Issue 4, Article No. 16 . . . . 11:1--11:2
Abhinav Jangda and
Uday Bondhugula An Effective Fusion and Tile Size Model
for PolyMage . . . . . . . . . . . . . . 12:1--12:27
Florian Frohn and
Matthias Naaf and
Marc Brockschmidt and
Jürgen Giesl Inferring Lower Runtime Bounds for
Integer Programs . . . . . . . . . . . . 13:1--13:50
Michael Coblenz and
Reed Oei and
Tyler Etzel and
Paulette Koronkevich and
Miles Baker and
Yannick Bloem and
Brad A. Myers and
Joshua Sunshine and
Jonathan Aldrich Obsidian: Typestate and Assets for Safer
Blockchain Programming . . . . . . . . . 14:1--14:82
Leandro T. C. Melo and
Rodrigo G. Ribeiro and
Breno C. F. Guimarães and
Fernando Magno Quintão Pereira Type Inference for C: Applications to
the Static Analysis of Incomplete
Programs . . . . . . . . . . . . . . . . 15:1--15:71
Peizun Liu and
Thomas Wahl and
Thomas Reps Interprocedural Context-Unbounded
Program Analysis Using Observation
Sequences . . . . . . . . . . . . . . . 16:1--16:34
Janwillem Swalens and
Joeri De Koster and
Wolfgang De Meuter Chocola: Composable Concurrency Language 17:1--17:56
Jiasi Shen and
Martin C. Rinard Active Learning for Inference and
Regeneration of Applications that Access
Databases . . . . . . . . . . . . . . . 18:1--18:119
Abu Naser Masud and
Björn Lisper Semantic Correctness of Dependence-based
Slicing for Interprocedural, Possibly
Nonterminating Programs . . . . . . . . 19:1--19:56
Marco Patrignani and
Deepak Garg Robustly Safe Compilation, an Efficient
Form of Secure Compilation . . . . . . . 1:1--1:41
David Sanan and
Yongwang Zhao and
Shang-Wei Lin and
Liu Yang CSim 2: Compositional Top-down
Verification of Concurrent Systems using
Rely-Guarantee . . . . . . . . . . . . . 2:1--2:46
David J. Pearce A Lightweight Formalism for Reference
Lifetimes and Borrowing in Rust . . . . 3:1--3:73
Colin S. Gordon Polymorphic Iterable Sequential Effect
Systems . . . . . . . . . . . . . . . . 4:1--4:79
Toru Takisaka and
Yuichiro Oyabu and
Natsuki Urabe and
Ichiro Hasuo Ranking and Repulsing Supermartingales
for Reachability in Randomized Programs 5:1--5:46
Elisabet Lobo-Vesga and
Alejandro Russo and
Marco Gaboardi A Programming Language for Data Privacy
with Accuracy Estimations . . . . . . . 6:1--6:42
Bernardo Toninho and
Nobuko Yoshida On Polymorphic Sessions and Functions: a
Tale of Two (Fully Abstract) Encodings 7:1--7:55
Jade Alglave and
Will Deacon and
Richard Grisenthwaite and
Antoine Hacquard and
Luc Maranget Armed Cats: Formal Concurrency Modelling
at Arm . . . . . . . . . . . . . . . . . 8:1--8:54
Weixin Zhang and
Yaozhu Sun and
Bruno C. D. S. Oliveira Compositional Programming . . . . . . . 9:1--9:61
Lun Liu and
Todd Millstein and
Madanlal Musuvathi Safe-by-default Concurrency for Modern
Programming Languages . . . . . . . . . 10:1--10:50
Graeme Gange and
Zequn Ma and
Jorge A. Navas and
Peter Schachte and
Harald Sòndergaard and
Peter J. Stuckey A Fresh Look at Zones and Octagons . . . 11:1--11:51
Matteo Busi and
Job Noorman and
Jo Van Bulck and
Letterio Galletta and
Pierpaolo Degano and
Jan Tobias Mühlberg and
Frank Piessens Securing Interruptible Enclaved
Execution on Small Microprocessors . . . 12:1--12:77
Peter Müller Introduction to the Special Section on
ESOP 2020 . . . . . . . . . . . . . . . 13:1--13:1
Carmine Abate and
Roberto Blanco and
Stefan Ciobâca and
Adrien Durier and
Deepak Garg and
Catalin Hrittcu and
Marco Patrignani and
Éric Tanter and
Jérémy Thibault An Extended Account of Trace-relating
Compiler Correctness and Secure
Compilation . . . . . . . . . . . . . . 14:1--14:48
Yusuke Matsushita and
Takeshi Tsukada and
Naoki Kobayashi RustHorn: CHC-based Verification for
Rust Programs . . . . . . . . . . . . . 15:1--15:54
Emanuele D'Osualdo and
Julian Sutherland and
Azadeh Farzan and
Philippa Gardner TaDA Live: Compositional Reasoning for
Termination of Fine-grained Concurrent
Programs . . . . . . . . . . . . . . . . 16:1--16:134
Frank S. de Boer and
Hans-Dieter A. Hiep Completeness and Complexity of Reasoning
about Call-by-Value in Hoare Logic . . . 17:1--17:35
Omar Inverso and
Ermenegildo Tomasco and
Bernd Fischer and
Salvatore La Torre and
Gennaro Parlato Bounded Verification of Multi-threaded
Programs via Lazy Sequentialization . . 1:1--1:50
Martin Hecker and
Simon Bischof and
Gregor Snelting On Time-sensitive Control Dependencies 2:1--2:37
Chaoqiang Deng and
Patrick Cousot The Systematic Design of Responsibility
Analysis by Abstract Interpretation . . 3:1--3:90
Maria I. Gorinova and
Andrew D. Gordon and
Charles Sutton and
Matthijs Vákár Conditional Independence by Typing . . . 4:1--4:54
Darya Melicher and
Anlun Xu and
Valerie Zhao and
Alex Potanin and
Jonathan Aldrich Bounded Abstract Effects . . . . . . . . 5:1--5:48
Leslie Lamport and
Stephan Merz Prophecy Made Simple . . . . . . . . . . 6:1--6:27
Meven Lennon-Bertrand and
Kenji Maillard and
Nicolas Tabareau and
Éric Tanter Gradualizing the Calculus of Inductive
Constructions . . . . . . . . . . . . . 7:1--7:82
Ori Lahav and
Udi Boker What's Decidable About Causally
Consistent Shared Memory? . . . . . . . 8:1--8:55
Qinheping Hu and
Rishabh Singh and
Loris D'Antoni Solving Program Sketches with Large
Integer Values . . . . . . . . . . . . . 9:1--9:28
Kensen Shi and
David Bieber and
Rishabh Singh TF-Coder: Program Synthesis for Tensor
Manipulations . . . . . . . . . . . . . 10:1--10:36
Yuanbo Li and
Qirun Zhang and
Thomas Reps Fast Graph Simplification for
Interleaved-Dyck Reachability . . . . . 11:1--11:28
Jacob R. Lorch and
Yixuan Chen and
Manos Kapritsos and
Haojun Ma and
Bryan Parno and
Shaz Qadeer and
Upamanyu Sharma and
James R. Wilcox and
Xueyuan Zhao Armada: Automated Verification of
Concurrent Code with Sound Semantic
Extensibility . . . . . . . . . . . . . 12:1--12:39
Nobuko Yoshida Introduction to the Special Issue on
ESOP 2021 . . . . . . . . . . . . . . . 13:1--13:1
Maximilian P. L. Haslbeck and
Peter Lammich For a Few Dollars More: Verified
Fine-Grained Algorithm Analysis Down to
LLVM . . . . . . . . . . . . . . . . . . 14:1--14:36
Patrick Baillot and
Alexis Ghyselen Types for Complexity of Parallel
Computation in Pi-calculus . . . . . . . 15:1--15:50
Jens Pagel and
Florian Zuleger Strong-separation Logic . . . . . . . . 16:1--16:40
Oren Ish-Shalom and
Shachar Itzhaky and
Noam Rinetzky and
Sharon Shoham Runtime Complexity Bounds Using
Squeezers . . . . . . . . . . . . . . . 17:1--17:36
Alex C. Keizer and
Henning Basold and
Jorge A. Pérez Session Coalgebras: a Coalgebraic View
on Regular and Context-free Session
Types . . . . . . . . . . . . . . . . . 18:1--18:45
Ankush Das and
Henry Deyoung and
Andreia Mordido and
Frank Pfenning Nested Session Types . . . . . . . . . . 19:1--19:45
Matthijs Vákár and
Tom Smeding CHAD: Combinatory Homomorphic Automatic
Differentiation . . . . . . . . . . . . 20:1--20:49
Friedrich Steimann Containerless Plurals: Separating Number
from Type in Object-Oriented Programming 21:1--21:??
Albert Mingkun Yang and
Tobias Wrigstad Deep Dive into ZGC: a Modern Garbage
Collector in OpenJDK . . . . . . . . . . 22:1--22:??
Dominique Devriese and
Marco Patrignani and
Frank Piessens Two Parametricities Versus Three
Universal Types . . . . . . . . . . . . 23:1--23:??
Yaoda Zhou and
Jinxu Zhao and
Bruno C. D. S. Oliveira Revisiting Iso-Recursive Subtyping . . . 24:1--24:??
Anindya Banerjee and
Ramana Nagasamudram and
David Naumann and
Mohammad Nikouei A Relational Program Logic with Data
Abstraction and Dynamic Framing . . . . 25:1--25:??
Vasco T. Vasconcelos and
Francisco Martins and
Hugo-Andrés López and
Nobuko Yoshida A Type Discipline for Message Passing
Parallel Programs . . . . . . . . . . . 26:1--26:??
Olivier Danvy The Tortoise and the Hare Algorithm for
Finite Lists, Compositionally . . . . . 1:1--1:??
Jingmei Hu and
Eric Lu and
David A. Holland and
Ming Kawaguchi and
Stephen Chong and
Margo Seltzer Towards Porting Operating Systems with
Program Synthesis . . . . . . . . . . . 2:1--2:??
Tobias Runge and
Marco Servetto and
Alex Potanin and
Ina Schaefer Immutability and Encapsulation for Sound
OO Information Flow Control . . . . . . 3:1--3:??
Ben Greenman and
Christos Dimoulas and
Matthias Felleisen Typed-Untyped Interactions: a
Comparative Analysis . . . . . . . . . . 4:1--4:??
Arthur Charguéraud and
Adam Chlipala and
Andres Erbsen and
Samuel Gruetter Omnisemantics: Smooth Handling of
Nondeterminism . . . . . . . . . . . . . 5:1--5:??
Hongyu Fan and
Zhihang Sun and
Fei He Satisfiability Modulo Ordering
Consistency Theory for SC, TSO, and PSO
Memory Models . . . . . . . . . . . . . 6:1--6:??
Adithya Murali and
Lucas Peña and
Christof Löding and
P. Madhusudan A First-order Logic with Frames . . . . 7:1--7:??
Matías Toro and
David Darais and
Chike Abuah and
Joseph P. Near and
Damián Árquez and
Federico Olmedo and
Éric Tanter Contextual Linear Types for Differential
Privacy . . . . . . . . . . . . . . . . 8:1--8:??
Xiaodong Jia and
Ashish Kumar and
Gang Tan A Derivative-based Parser Generator for
Visibly Pushdown Grammars . . . . . . . 9:1--9:??
Matteo Basso and
Aleksandar Prokopec and
Andrea Ros\`a and
Walter Binder Optimization-Aware Compiler-Level Event
Profiling . . . . . . . . . . . . . . . 10:1--10:??
Eugene Yip and
Alain Girault and
Partha S. Roop and
Morteza Biglari-Abhari Synchronous Deterministic Parallel
Programming for Multi-Cores with ForeC 11:1--11:??
Alex Sanchez-Stern and
Emily First and
Timothy Zhou and
Zhanna Kaufman and
Yuriy Brun and
Talia Ringer Passport: Improving Automated Formal
Verification Using Identifiers . . . . . 12:1--12:??
Luigi Soares and
Michael Canesche and
Fernando Magno Quintão Pereira Side-channel Elimination via Partial
Control-flow Linearization . . . . . . . 13:1--13:??
Elizabeth Scott and
Adrian Johnstone and
Robert Walsh Multiple Input Parsing and Lexical
Analysis . . . . . . . . . . . . . . . . 14:1--14:??
Philipp G. Haselwarter and
Exequiel Rivas and
Antoine Van Muylder and
Théo Winterhalter and
Carmine Abate and
Nikolaj Sidorenco and
Catalin Hritcu and
Kenji Maillard and
Bas Spitters SSProve: a Foundational Framework for
Modular Cryptographic Proofs in Coq . . 15:1--15:??
Dongkwon Lee and
Woosuk Lee and
Hakjoo Oh and
Kwangkeun Yi Optimizing Homomorphic Evaluation
Circuits by Program Synthesis and
Time-bounded Exhaustive Search . . . . . 16:1--16:??
David Richter and
David Kretzler and
Pascal Weisenburger and
Guido Salvaneschi and
Sebastian Faust and
Mira Mezini Prisma : a Tierless Language for
Enforcing Contract-client Protocols in
Decentralized Applications . . . . . . . 17:1--17:??
Kesha Hietala and
Robert Rand and
Liyi Li and
Shih-Han Hung and
Xiaodi Wu and
Michael Hicks A Verified Optimizer for Quantum
Circuits . . . . . . . . . . . . . . . . 18:1--18:??
Michele Chiari and
Dino Mandrioli and
Francesco Pontiggia and
Matteo Pradella A Model Checker for Operator Precedence
Languages . . . . . . . . . . . . . . . 19:1--19:??
Maja Vukasovic and
Aleksandar Prokopec Exploiting Partially Context-sensitive
Profiles to Improve Performance of Hot
Code . . . . . . . . . . . . . . . . . . 20:1--20:??
Aleksander Boruch-Gruszecki and
Martin Odersky and
Edward Lee and
Ondrej Lhoták and
Jonathan Brachthäuser Capturing Types . . . . . . . . . . . . 21:1--21:??
Dimitrios J. Economou and
Neel Krishnaswami and
Jana Dunfield Focusing on Refinement Typing . . . . . 22:1--22:??
Saverio Giallorenzo and
Fabrizio Montesi and
Marco Peressotti Choral: Object-oriented Choreographic
Programming . . . . . . . . . . . . . . 1:1--1:??
Julian Haas and
Ragnar Mogk and
Elena Yanakieva and
Annette Bieniusa and
Mira Mezini LoRe: a Programming Model for Verifiably
Safe Local-first Software . . . . . . . 2:1--2:??
Crystal Chang Din and
Reiner Hähnle and
Ludovic Henrio and
Einar Broch Johnsen and
Violet Ka I. Pun and
S. Lizeth Tapia Tarifa Locally Abstract, Globally Concrete
Semantics of Concurrent Programming
Languages . . . . . . . . . . . . . . . 3:1--3:??
Benno Stein and
Bor-Yuh Evan Chang and
Manu Sridharan Interactive Abstract Interpretation with
Demanded Summarization . . . . . . . . . 4:1--4:??
Roberto Giacobazzi and
Isabella Mastroeni and
Elia Perantoni Adversities in Abstract Interpretation
--- Accommodating Robustness by Abstract
Interpretation . . . . . . . . . . . . . 5:1--5:??
Aman Nougrahiya and
V. Krishna Nandivada Homeostasis: Design and Implementation
of a Self-Stabilizing Compiler . . . . . 6:1--6:??
Meghana Aparna Sistla and
Swarat Chaudhuri and
Thomas Reps CFLOBDDs: Context-Free-Language Ordered
Binary Decision Diagrams . . . . . . . . 7:1--7:??
Ruyi Ji and
Yuwei Zhao and
Yingfei Xiong and
Di Wang and
Lu Zhang and
Zhenjiang Hu Decomposition-based Synthesis for
Applying Divide-and-Conquer-like
Algorithmic Paradigms . . . . . . . . . 8:1--8:??
Frank de Boer and
Einar Broch Johnsen and
Violet Ka I. Pun and
Silvia Lizeth Tapia Tarifa Proving Correctness of Parallel
Implementations of Transition System
Models . . . . . . . . . . . . . . . . . 9:1--9:??
Ari Rasch (De\slash Re)-Composition of
Data-Parallel Computations via
Multi-Dimensional Homomorphisms . . . . 10:1--10:??
Flavio Ascari and
Roberto Bruni and
Roberta Gori Limits and Difficulties in the Design of
Under-Approximation Abstract Domains . . 11:1--11:??
Iacovos G. Kolokasis and
Giannos Evdorou and
Shoaib Akram and
Christos Kozanitis and
Anastasios Papagiannis and
Foivos S. Zakkak and
Polyvios Pratikakis and
Angelos Bilas TeraHeap: Exploiting Flash Storage for
Mitigating DRAM Pressure in Managed Big
Data Frameworks . . . . . . . . . . . . 12:1--12:??
Marco Patrignani and
Robert Künnemann and
Riad S. Wahby and
Ethan Cecchetti Universal Composability Is Robust
Compilation . . . . . . . . . . . . . . 13:1--13:??
Jenna DiVincenzo and
Ian McCormack and
Conrad Zimmerman and
Hemant Gouni and
Jacob Gorenburg and
Jan-Paul Ramos-Dávila and
Mona Zhang and
Joshua Sunshine and
Éric Tanter and
Jonathan Aldrich Gradual C0: Symbolic Execution for
Gradual Verification . . . . . . . . . . 14:1--14:??
Jason Z. S. Hu and
Brigitte Pientka A Layered Approach to Intensional
Analysis in Type Theory . . . . . . . . 15:1--15:??