[Agda] Re: Normalization by evaluation, plain Agda types and impredicativity.

[Andrea Vezzosi]

No, I don't think there's a paper for it

On Mon, Sep 29, 2014 at 4:55 PM, flicky frans <flickyfrans at gmail.com> wrote:
> Thanks for the answers.
>
>> Here is a (historical) reference describing your technique for System F-omega, albeit before the time of Agda...
>
> It's similar, but not exactly the same. Their representation is
> predicative (kinds are inferred by a compiler) and `Term' is not an
> inductive-recursive type.
>
>> I don't know how relevant it is to this thread but there's also the
>> style from McBride's "Outrageous but Meaningful Coincidences:
>> Dependent type-safe syntax and evaluation".
>
> This is related, but again, there is an encoded universe with a
> decoding function instead of plain Agda types.
> Do you know, is there some accompanying paper for your [1]?