[PRL] Type-directed partial evaluation

[David Herman]

Is this the paper?

     http://citeseer.nj.nec.com/cartwright92observable.html

Thanks,
Dave

On Thursday, January 8, 2004, at 06:03 PM, Matthias Felleisen wrote:

> As you pointed out in the old papers, denotations are compiled code.
>
> The denotations in SEQ (the category of domains that I developed with 
> Curien and Corky) allows a FA semantics for PCF with catch (or a 
> restricted version of callcc). Inside the FA proof, there is an 
> algorithm -- not unlike Danvy's -- that resurrects the source code of 
> a function. You use catch to provide the coroutining that is necessary 
> between functionals of rank 2 and higher (see my first lecture in 369) 
> and their arguments. That's the rough idea. I claim it is an algorithm 
> (even though I only have words right now) because I can do it 
> systematically and because it always terminates.
>
> Rama extended this to the infinite case in a joint paper that we 
> presented at some too obscure conference in the Netherlands. SEQ is 
> thus the only known category that presents finite elements in a 
> constructive, enumerable manner, allows a FA proof, therefore allows 
> the textual representation of all finite elements, and allows full 
> expressiveness of all infinite computable elements in the domain on 
> top. (Naturally, we can't represent infinite non-computable elements 
> from the "code basis" aka domains.) I therefore claim that SEQ domains 
> are far superior to the Abramsky-Hyland clan production. :-)
>
> -- Matthias
>
>
> On Thursday, January 8, 2004, at 05:58 PM, Mitchell Wand wrote:
>
>>> Take PCF instead of Scheme. Take good(tm) domains instead of
>>> target-machine code (and read some of Mitch's old papers from the 
>>> early
>>> 80s). Then I can create source text for all infinite computable
>>> "compiled codes" using call/cc. Though I have to admit that the
>>> algorithm is burried in two papers
>>> and I only know the one for finite computable "codes" reasonable well
>>> to do it on the spot.
>>
>>> -- Matthias
>>
>> Umm, tell us more?
>>
>> --Mitch
>