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

[Kenichi Asai]

> 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