racket

History

Robby Findler 0c6e0a11cf removed ambiguity from the cont-mark-transform's "a" non-terminal Redex no longer has extra checks to eliminate redundant matches (as those checks are prohibitively expensive for the lambdajs model) so redundancy in the grammar can, when combined with context decomposition or named patterns, lead to significant slowdowns		2012-01-09 12:57:22 -06:00
..
cont-mark-transform	removed ambiguity from the cont-mark-transform's "a" non-terminal	2012-01-09 12:57:22 -06:00
define-judgment-form	Drops `traces' call to make the file DrDr-friendly	2011-08-15 12:46:14 -05:00
delim-cont	Fix another bunch of "language" typos.	2011-08-26 05:26:46 -04:00
list-machine	add the List Machine benchmark by Appel, Dockins, and Leroy	2011-12-10 01:34:58 -06:00
r6rs	remove (broken) attempt at optimization Jay suggested	2012-01-08 12:13:37 -06:00
racket-machine	".ss" -> ".rkt" scan done.	2011-07-02 10:37:53 -04:00
arithmetic.rkt	Rackety	2011-01-17 17:19:37 -06:00
beginner.rkt	Fixes bugs in error transitions	2011-03-29 15:57:50 -05:00
cbn-letrec.rkt	Add evaluation contexts for by-need letrec calculus as an example	2011-09-19 12:20:45 -05:00
church.rkt	Rackety	2011-01-17 17:19:37 -06:00
combinators.rkt	Rackety	2011-01-17 17:19:37 -06:00
compatible-closure.rkt	Rackety	2011-01-17 17:19:37 -06:00
contracts.rkt	Rackety	2011-01-17 17:19:37 -06:00
info.rkt	rename all files .ss -> .rkt	2010-04-27 16:50:15 -06:00
letrec.rkt	".ss" -> ".rkt" scan done.	2011-07-02 10:37:53 -04:00
omega.rkt	".ss" -> ".rkt" scan done.	2011-07-02 10:37:53 -04:00
pi-calculus.rkt	Rackety	2011-01-17 17:19:37 -06:00
README	add the List Machine benchmark by Appel, Dockins, and Leroy	2011-12-10 01:34:58 -06:00
semaphores.rkt	Rackety	2011-01-17 17:19:37 -06:00
stlc.rkt	Updates STLC example to use define-judgment-form	2011-08-10 12:24:01 -05:00
subject-reduction.rkt	Rackety	2011-01-17 17:19:37 -06:00
subst.rkt	Rackety	2011-01-17 17:19:37 -06:00
threads.rkt	Fixes a bug in the deref rule	2011-03-29 16:05:54 -05:00
types.rkt	".ss" -> ".rkt" scan done.	2011-07-02 10:37:53 -04:00

README

The examples subcollection contains several small languages 
to demonstrate various different uses of PLT Redex:

  arithmetic.rkt: an arithmetic language with every
  possible order of evaluation

  beginner.rkt: a PLT Redex implementation of (much of) the
  beginning student teaching language.

  cbn-letrec.rkt: the definition of evaluation contexts in Ariola and
  Felleisen's call-by-need letrec calculus

  church.rkt: Church numerals with call by name
  normal order evaluation

  combinators.rkt: fills in the gaps in a proof in
  Barendregt that i and j (defined in the file) are
  a combinator basis

  compatible-closure.rkt: an example use of compatible
  closure. Also, one of the first examples from Matthias
  Felleisen and Matthew Flatt's monograph

  cont-mark-transform/: the continuation mark transformation from
  McCarthy's ICFP '09 paper “Automatically RESTful Web Applications
  Or, Marking Modular Serializable Continuations" 

  contracts.rkt: A core contract calculus, including blame, 
  with function contracts, (eager) pair contracts, 
  and a few numeric predicates

  define-judgment-form: example uses of `define-judgment-form'

  delim-cont/: The model from Flatt, Yu, Findler, and Felleisen's ICFP
  '07 paper "Adding Delimited and Composable Control to a Production
  Programming Environment"

  letrec.rkt: shows how to model letrec with a store and
  some infinite looping terms

  list-machine/: the List Machine benchmark by Appel, Dockins, and
  Leroy.

  omega.rkt: the call by value lambda calculus with call/cc.
  Includes omega and two call/cc-based infinite loops, one of
  which has an ever-expanding term size and one of which has
  a bounded term size.

  pi-calculus.rkt: a formulation of the pi calculus, following
  Milner's 1990 paper, "Functions as Processes"

  racket-machine/: an operational semantics for (much of) Racket
  bytecode

  r6rs/: an implementation of the R6RS Scheme formal semantics

  semaphores.rkt: a simple threaded language with semaphores

  stlc.rkt: a semantics for a typed CBV language with multi-argument
  functions, conditionals, and addition

  subject-reduction.rkt: demos traces/pred that type checks
  the term.

  threads.rkt: shows how non-deterministic choice can be
  modeled in a reduction semantics. Contains an example use
  of a simple alternative pretty printer.

  types.rkt: shows how the simply-typed lambda calculus's
  type system can be written as a rewritten system (see
  Kuan, MacQueen, Findler in ESOP 2007 for more).