Idealized Algol

Idealized Algol (IA) is a core calculus that captures the 'essence' of Algol-like languages. It is essentially a simply-typed \lambda-calculus with recursion and additional primitives for a first-order store with local variables.

IA appears to have been introduced by Peter O'Hearn in a 1996 paper published in the Journal of Functional Programming O'Hearn 1996.

It is possible to 'modernise' IA using more recent idea from effectful calculi. The result is called Modernized Algol.

Syntax

The types of IA are given by the usual types of PCF, as well as a type of variables and a type of commands:

  A, B \Coloneqq \textsf{Nat} \mid \textbf{Bool} \mid A \to B \mid \textsf{Var} \mid \textsf{Comm}

We also extend PCF with constructs for reading and writing from the store, for making new variables, and for sequential composition of commands:

\frac{
\Gamma \vdash M : \textsf{Var}
}{
\Gamma \vdash \textsf{deref}(M) : \textsf{Nat}
}
\quad
\frac{
\Gamma \vdash M : \textsf{Var}
\quad
\Gamma \vdash N : \textsf{Nat}
}{
\Gamma \vdash M \coloneqq N : \textsf{Comm}
}
\quad
\frac{
\Gamma \vdash M : \textsf{Nat}
\quad
\Gamma, x : \textsf{Var} \vdash N : \textsf{Comm}
}{
\Gamma \vdash \textsf{new}(M; x.\, N) : \textsf{Comm}
}

\frac{
\Gamma \vdash M : \textsf{Comm}
\quad
\Gamma \vdash N : \textsf{Comm}
}{
\Gamma \vdash M; N : \textsf{Comm}
}

Semantics

Early semantic models of languages like IA used the so-called marked store models.

Many models of IA from the 1990s suffered from a serious snapback problem. O'Hearn 1998 criticizes all of the following models for this:

the functor category models of Oles 1982
the model of Sieber 1996
the parametricity model of O'HEarn and Tennent 1995

References

Idealized Algol was first introduced in

O’Hearn, Peter W. 1996. ‘Note on Algol and Conservatively Extending Functional Programming’. Journal of Functional Programming 6 (1): 171–80. https://doi.org/10.1017/S0956796800001611.

@article{ohearn_note_1996,
	title = {Note on {Algol} and conservatively extending functional programming},
	volume = {6},
	doi = {10.1017/S0956796800001611},
	number = {1},
	journal = {Journal of Functional Programming},
	author = {O'Hearn, Peter W.},
	year = {1996},
	pages = {171--180},
}

Early-period work on the semantics of IA consists of so-called marked store models.
Mid-period work on the semantics of IA includes

O’Hearn, P. W., and R. D. Tennent. 1995. ‘Parametricity and Local Variables’. Journal of the ACM 42 (3): 658–709. https://doi.org/10.1145/210346.210425.

@article{ohearn_parametricity_1995,
	title = {Parametricity and local variables},
	volume = {42},
	doi = {10.1145/210346.210425},
	number = {3},
	journal = {Journal of the ACM},
	author = {O'Hearn, P. W. and Tennent, R. D.},
	year = {1995},
	pages = {658--709}
}

Sieber, Kurt. 1996. ‘Full Abstraction for the Second Order Subset of an Algol-like Language’. Theoretical Computer Science 168 (1): 155–212. https://doi.org/10.1016/S0304-3975(96)00066-7. This is the journal version of the paper from the Algol-like languages volume, which is the conference version.

@article{sieber_full_1996,
	title = {Full abstraction for the second order subset of an {Algol}-like language},
	volume = {168},
	doi = {10.1016/S0304-3975(96)00066-7},
	number = {1},
	journal = {Theoretical Computer Science},
	author = {Sieber, Kurt},
	year = {1996},
	pages = {155--212},
	annote = {This is the JOURNAL version of the article from 1994. “Algol-like languages” contains the conference version.
}
}