Illustrative Examples

This section illustrates mechanisation of denotational semantics in Agda with three examples, all using the postulated notation for domains and their associated operations: the Untyped Lambda-Calculus, PCF: A Programming Language for Computable Functions, and Scm: A Sublanguage of Scheme.

{-# OPTIONS --rewriting --confluence-check --lossy-unification #-}

module Examples where

import Examples.LC
import Examples.PCF
import Examples.Scm