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

[flicky frans]

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