Article ID Journal Published Year Pages File Type
436343 Theoretical Computer Science 2008 12 Pages PDF
Abstract

The parametric lambda calculus subsumes different existing λ-calculi, in particular the classical λβ-calculus and the λβv-calculus of Plotkin. Previously established results on the parametric calculus, such as confluence and standardization, are primarily syntactical. In this paper our attention is mainly addressed to semantics, although we start again from a syntactical point of view. We propose an analysis of the notion of contextual preorders of usual operational semantics. Given a contextual preorder, we build a parametric complete lattice based on a closure operator. This lattice provides a fully abstract model for the considered preorder, via a completion.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics