As the last article of this series, today we will discuss the denotational semantics for imperative programs. Specifically, we will check out how to apply CPO model on the $\text{while}$ programs i...

In this article, we consider the domain-theoretic semantics of PCF. This provides some insight into the properties of CPOs, and also provides the basis for semantic reasoning about PCF. We show so...

Fixed Points and the Full Continuous Hierarchy Our current motivation for studying domain-theoretic models is to construct Henkin models of typed lambda calculi with fixed-point operators. The t...

In the last article, we provides a full set-theoretic interpretation for typed lambda calculus based on the Henkin model. However, the function recursion in PCF is hard to model from a pure set vie...

In this series, let us check out the denotational semantics of typed lambda calculus, which uses models to express the meaning of terms. For most logical systems, a model provides a mechanism for ...

In preceding articles, we considered functional programs that do not contain assignment or other operations that change the values of identifiers. In computer science, of course, it is more common ...

In this article, we introduce a new mathematical framework which is simpler than typed lambda calculus, called universal algebra (or equational logic). This framework will be useful when we model i...

This article introduces the axiomatic semantics of typed lambda calculus. Recall that “axiomatic semantics consists of a proof system for deducing properties of programs and their parts.” The equat...

PLDI, whose full name is the Conference on Programming Language Design and Implementation, is held today in Copenhagen, Denmark this year. It is the most famous conference in the programming langua...

Today, we are going to present the pure simply-typed lambda calculus. PCF is extended from this system by adding natural numbers, booleans, and fixed-point operators. In previous articles, we used...