README
1The examples subcollection contains several small languages
2to demonstrate various different uses of PLT Redex:
3
4 arithmetic.rkt: an arithmetic language with every
5 possible order of evaluation
6
7 beginner.rkt: a PLT Redex implementation of (much of) the
8 beginning student teaching language.
9
10 cbn-letrec.rkt: the definition of evaluation contexts in Ariola and
11 Felleisen's call-by-need letrec calculus
12
13 church.rkt: Church numerals with call by name
14 normal order evaluation
15
16 combinators.rkt: fills in the gaps in a proof in
17 Barendregt that i and j (defined in the file) are
18 a combinator basis
19
20 compatible-closure.rkt: an example use of compatible
21 closure. Also, one of the first examples from Matthias
22 Felleisen and Matthew Flatt's monograph
23
24 cont-mark-transform/: the continuation mark transformation from
25 McCarthy's ICFP '09 paper “Automatically RESTful Web Applications
26 Or, Marking Modular Serializable Continuations"
27
28 contracts.rkt: A core contract calculus, including blame,
29 with function contracts, (eager) pair contracts,
30 and a few numeric predicates
31
32 define-judgment-form: example uses of `define-judgment-form'
33
34 delim-cont/: The model from Flatt, Yu, Findler, and Felleisen's ICFP
35 '07 paper "Adding Delimited and Composable Control to a Production
36 Programming Environment"
37
38 lazy.rkt: big step semantics for lazy evaluation by Launchbury, POPL'93
39
40 let-poly.rkt: lambda calculus with list constants, let-polymorphism
41 and type inference
42
43 letrec.rkt: shows how to model letrec with a store and
44 some infinite looping terms
45
46 list-machine/: the List Machine benchmark by Appel, Dockins, and
47 Leroy.
48
49 omega.rkt: the call by value lambda calculus with call/cc.
50 Includes omega and two call/cc-based infinite loops, one of
51 which has an ever-expanding term size and one of which has
52 a bounded term size.
53
54 pi-calculus.rkt: a formulation of the pi calculus, following
55 Milner's 1990 paper, "Functions as Processes"
56
57 poly-stlc.rkt: a polymorphic lambda calculus with list constants
58
59 racket-machine/: an operational semantics for (much of) Racket
60 bytecode
61
62 r6rs/: an implementation of the R6RS Scheme formal semantics
63
64 semaphores.rkt: a simple threaded language with semaphores
65
66 stlc.rkt: a semantics for a typed CBV language with multi-argument
67 functions, conditionals, and addition
68
69 stlc+lists.rkt: simply typed lambda calculus with list and
70 number types
71
72 stlc+lists+subst.rkt: identical to stlc+lists.rkt except that
73 capture avoiding substitution is defined explicitly
74
75 subject-reduction.rkt: demos traces/pred that type checks
76 the term.
77
78 threads.rkt: shows how non-deterministic choice can be
79 modeled in a reduction semantics. Contains an example use
80 of a simple alternative pretty printer.
81
82 types.rkt: shows how the simply-typed lambda calculus's
83 type system can be written as a rewritten system (see
84 Kuan, MacQueen, Findler in ESOP 2007 for more).
85