Algol-like Languages

1. Front Matter

   Pages i-vii

   PDF

2. Functor-Category Semantics

   1. Front Matter

      Pages 1-1

      PDF

   2. Functor Categories and Store Shapes

      • Frank J. Oles

      Pages 3-12

   3. Using Functor Categories to Generate Intermediate Code

      • John C. Reynolds

      Pages 13-38

3. Specification Logic

   1. Front Matter

      Pages 39-39

      PDF

   2. Semantical Analysis of Specification Logic

      • Robert D. Tennent

      Pages 41-64

   3. Semantical Analysis of Specification Logic, 2

      • Peter W. O’Hearn, Robert D. Tennent

      Pages 65-93

4. Procedures and Local Variables

   1. Front Matter

      Pages 95-95

      PDF

   2. Full Abstraction for the Second-Order Subset of an Algol-like Language

      • Kurt Sieber

      Pages 97-107

   3. Parametricity and Local Variables

      • Peter W. O’Hearn, Robert D. Tennent

      Pages 109-163

   4. Reasoning About Local Variables with Operationally-Based Logical Relations

      • Andrew M. Pitts

      Pages 165-185

5. Interference, Irreversibility, and Concurrency

   1. Front Matter

      Pages 187-187

      PDF

   2. Syntactic Control of Interference Revisited

      • Peter W. O’Hearn, A. John Power, Makoto Takeyama, Robert D. Tennent

      Pages 189-225

   3. Global State Considered Unnecessary: Introduction to Object-Based Semantics

      • Uday S. Reddy

      Pages 227-295

   4. Linearity, Sharing and State: A Fully Abstract Game Semantics for Idealized Algol with Active Expressions

      • Samson Abramsky, Guy McCusker

      Pages 297-329

   5. The Essence of Parallel Algol

      • Stephen Brookes

      Pages 331-348

6. Back Matter

   Pages 349-349

   PDF

To construct a compiler for a modern higher-level programming languagel one needs to structure the translation to a machine-like intermediate language in a way that reflects the semantics of the language. little is said about such struc­ turing in compiler texts that are intended to cover a wide variety of program­ ming languages. More is said in the Iiterature on semantics-directed compiler construction [1] but here too the viewpoint is very general (though limited to 1 languages with a finite number of syntactic types). On the other handl there is a considerable body of work using the continuation-passing transformation to structure compilers for the specific case of call-by-value languages such as SCHEME and ML [21 3]. ln this paperl we will describe a method of structuring the translation of ALGOL-like languages that is based on the functor-category semantics devel­ oped by Reynolds [4] and Oles [51 6]. An alternative approach using category theory to structure compilers is the early work of F. L. Morris [7]1 which anticipates our treatment of boolean expressionsl but does not deal with procedures. 2 Types and Syntax An ALGOL-like language is a typed lambda calculus with an unusual repertoire of primitive types. Throughout most of this paper we assume that the primi­ tive types are comm(and) int(eger)exp(ression) int(eger)acc(eptor) int(eger)var(iable) I and that the set 8 of types is the least set containing these primitive types and closed under the binary operation -.

• ALGOL
• Computer
• Languages
• ML
• Turing
• Variable
• calculus
• code
• compiler
• compiler construction
• lambda calculus
• logic
• programming language
• semantics

• Dept. of Computer Science, Queen Mary & Westfield College, England

  Peter W. O’Hearn

• Dept. of Computing and Information Science, Queen’s University, Kingston, Canada

  Robert D. Tennent

Policies and ethics