[racket] [redex] traces for derivation trees

From: Eric Tanter (etanter at dcc.uchile.cl)
Date: Wed Mar 7 14:16:40 EST 2012


As I'm enjoying the new `define-judgment-form' in Redex, I started to dream about an equivalent of `traces' for `judgment-holds'. 

I'm going to try to use Redex in a course based on Pierce's TAPL, and once students see `traces' for reduction relations, they will be a bit disappointed by the text-based output for typing derivations that one can obtain by using `current-traced-metafunctions'.

Is there something like that already? if not, does it sound feasible?


-- Éric

Posted on the users mailing list.