[Haskell-cafe] Type-indexed expressions with fixpoint

[pbrowne]

oleg at okmij.org wrote:
> Brent Yorgey wrote:
> 
> John Reynolds showed long ago that any higher-order language can be
> encoded in first-order. We witness this every day: higher-order
> language like Haskell is encoded in first-order language (machine
> code). The trick is just to add a layer of interpretive overhead -- I
> mean, a layer of interpretation. The closure conversion on type level
> was shown in
>   http://okmij.org/ftp/Computation/lambda-calc.html#haskell-type-level
> 
Brent,
Do you have the reference for Reynolds higher-order to first-order encoding.

Regards,
Pat