本文记录如何在 VMware Fusion 中，让 Ubuntu 虚拟机通过 Mac 上的 VPN/代理软件访问 Google、GitHub、apt 源等外网资源。 实验环境示例： 宿主机：macOS 虚拟机软件：VMware Fusion 虚拟机系统：Ubuntu Server VMware 网络模式：Share with my Mac Mac 代理软件：Flyi...

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...