[PRL] Type-directed partial evaluation

[Matthias Felleisen]

Look for Curien on this page:
   http://www.ccs.neu.edu/scheme/pubs/

BTW, the situation corresponds to "sourcing" an optimized piece of code.

-- Matthias

On Thursday, January 8, 2004, at 08:38 PM, David Herman wrote:

> 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
>>