Skip to content
This repository


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

PCF with Contracts and Symbolic Values

branch: master

Fetching latest commit…


Cannot retrieve the latest commit at this time

Octocat-spinner-32 cpcf
Octocat-spinner-32 pcf
Octocat-spinner-32 scpcf
Octocat-spinner-32 scribblings
Octocat-spinner-32 spcf
Octocat-spinner-32 tests
Octocat-spinner-32 .gitignore

PCF with Contracts and Symbolic Values

This collection implements four core programming languages, useful for studying PCF, contracts, and symbolic execution:

  • PCF: a core typed language (with natural numbers, errors and recursion).

  • Symbolic PCF ('PCF): an extension of PCF endowed with a notion of "symbolic values", written (• T), which represents an abstraction of all values of type T.

  • Contract PCF (CPCF): an extension of PCF endowed with behavioral software contracts. Contracts include arbitrary predicates written in PCF and higher-order contracts, written (C ... -> C). The monitor of a contract against a computation is written (C ⚖ M). When a contract fails, blame is signalled and indicates who is to blame.

  • Symbolic CPCF ('CPCF): an extension of Contract PCF endowed with symbolic values written (• T C ...), which represents an abstraction of all values of type T satisfying contracts C ....

These languages are available as #lang languages that include static type checking:

#lang pcf <option>
#lang spcf <option>
#lang cpcf <option>
#lang scpcf <option>


option ::= | traces | stepper

These languages are also available as Redex models.



  • LANG/examples.rkt: examples written in each language.
  • LANG/redex.rkt: Redex models of each language.
  • LANG/lang/: implements #lang LANG.
  • tests/LANG/: tests for each language.

Installation and testing

You will need Racket or later.

% raco pkg install pcf
Something went wrong with that request. Please try again.