redex

Redex model of World Age Calculus

PLT Redex is a racket DSL for modeling programming language semantics.

Introductory materials:

• PLT Redex FAQ by Ben Greenman and Sam Caldwell
• Experimenting with Languages in Redex by William J. Bowman
• Redex Tutorial

Dependencies

• Racket with Redex

Source Code

• core folder with the core operational semantics:

  • wa-surface.rkt surface language WA (expressions, types, subtyping);

  • wa-full.rkt semantics of the calculus WA-full (aux definitions such as typeof and primops, and small-step reduction relation);

• optimizations folder with program optimizations for world age calculus:

  • wa-optimized.rkt the optimization semantics of world age, WA-opt (optimization algorithm, definition of correctness of optimization, and world age semantics employing optimizations);

• wa-examples.rkt example expressions;

• tests folder with tests:

  • wa-tests.rkt hand-written unit-tests for the grammar and core semantics;

  • wa-prop-tests.rkt random testing (currently, only for determinism of the semantics);

  • wa-optimized-tests.rkt hand-written unit tests to validate the equivalence of optimized and unoptimized expressions;

Note. File attic/wa-full.rkt contains a direct implementation of finding applicable methods, without an auxiliary latest function.