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 typeT
. -
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 typeT
satisfying contractsC ...
.
These languages are available as #lang
languages that include static
type checking:
#lang pcf <option>
#lang spcf <option>
#lang cpcf <option>
#lang scpcf <option>
where
option ::= | traces | stepper
These languages are also available as Redex models.
http://dvanhorn.github.com/pcf/
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.
You will need Racket 5.3.1.9 or later.
% raco pkg install pcf