Skip to content
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
61 lines (43 sloc) 1.65 KB

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
You can’t perform that action at this time.