[racket] TR: Making recursive types as subtypes of non-recursive types

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Thu Feb 23 08:39:45 EST 2012

On Feb 22, 2012, at 11:12 PM, Neil Toronto wrote:

> It would be fun to try to port Coq's constructive ordinals to phantom types in TR, though, to see how far I could get with occurrence typing instead of dependent typing.


If you got far, it would validate our gut-level conjecture of 'practical dependence' for TR. 

Zermelo–Fraenkel with Choice forever :-] 

Send me a copy of the paper. 



Posted on the users mailing list.