PLS Lab

Webbed models of the untyped \lambda-calculus

Many models of the untyped \lambda-calculus are so-called webbed models. This means that the domain over which the \lambda-calculus is interpreted is a substructure of the algebraic lattice

(\mathcal{P}(D), \subseteq)

for some set D. The set D is called the web of the model.

The terminology appears to be due to Berline 2000.

The construction of many webbed models is fairly elementary. Thus, they are often used in the semantics of various applied calculi.

Webbed models include:

References

Berline, Chantal. ‘From Computation to Foundations via Functions and Application: The λ-Calculus and Its Webbed Models’. Theoretical Computer Science 249, no. 1 (2000): 81–161. https://doi.org/10.1016/S0304-3975(00)00057-8.
@article{berline_2000,
	title = {From computation to foundations via functions and application: The λ-calculus and its webbed models},
	volume = {249},
	doi = {10.1016/S0304-3975(00)00057-8},
	pages = {81--161},
	number = {1},
	journaltitle = {Theoretical Computer Science},
	author = {Berline, Chantal},
	date = {2000},
}
###

::
:::