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

[Andrea Vezzosi]

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".
There you define first-order terms but higher-order semantic types to
index them with.

And for NbE there are at least two quite different examples:
- [1] where the semantic types use the NbE semantic domain themselves.
- [2] where the semantic types are defined a priori by mapping into
corresponding Agda's types.

[1] https://personal.cis.strath.ac.uk/conor.mcbride/fooling/DepNobby.agda
[2] http://www.cse.chalmers.se/~nad/listings/dependently-typed-syntax/README.DependentlyTyped.NBE.html

On Sun, Sep 28, 2014 at 1:26 PM, flicky frans <flickyfrans at gmail.com> wrote:
>> Hi.  I formalized TDPE (= NbE) for simply-typed lambda calculus (but
>> without any dependent types as you requested) in Coq and Agda using
>> PHOAS, if it helps:
>
> It helps, thanks. Formalising STLC using PHOAS is what I've started
> from. There is a very similar development by Nils Anders Danielsson,
> but there aren't completeness and soundness proofs [1].
>
> [1] http://www.cse.chalmers.se/~nad/listings/simply-typed/HOAS.SimplyTyped.html
>
> 2014-09-28 15:03 GMT+04:00, Kenichi Asai <asai at is.ocha.ac.jp>:
>>> Hello. I am searching for a paper, that describes normalization by
>>> evaluation for roughly this representation of the lambda-calculus:
>>
>> Hi.  I formalized TDPE (= NbE) for simply-typed lambda calculus (but
>> without any dependent types as you requested) in Coq and Agda using
>> PHOAS, if it helps:
>>
>> Hirota, N., and K. Asai "Formalizing a Correctness Property of a
>> Type-Directed Partial Evaluator"
>> http://dl.acm.org/citation.cfm?id=2541572
>> http://pllab.is.ocha.ac.jp/~asai/papers/ (for Coq/Agda files)
>>
>> Sincerely,
>>
>> --
>> Kenichi Asai
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda