Background

This section first recalls the main features of Scott–Strachey denotational semantics, and summarises the notation conventionally used in denotational descriptions of programming languages. It then mentions significant features of the Agda language, and briefly explains some Agda syntax used in the subsequent sections.

module Background where
  import Background.Denotational-Semantics
  import Background.Agda