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

[Andreas Abel]

Here is a (historical) reference describing your technique for System 
F-omega, albeit before the time of Agda...

@TechReport{pierce:leap,
   author = 	 {Benjamin Pierce and Scott Dietzen and Spiro Michaylov},
   title = 	 {Programming in Higher-Order Typed Lambda-Calculi},
   institution =  {Carnegie Mellon University},
   year = 	 1989,
   key =		 {CMU-CS-89-111}
}


On 28.09.2014 13:26, flicky frans 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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/