[Agda] Re: [yoshiki] Re: AIM 6

[Peter Dybjer]

Dear Norio,

I will speak at the Proglog-CVS video seminar on Wednesday. The title is

"Recent news on normalization by evaluation for type theory"

The talk will begin at 9.15 am Swedish time (note that our clocks just
changed). Before that at 9.00 am we will have a short overview of "latest
news at AIST and Chalmers".

NOTE. We will only use the Marratech system this time, and not the video
conference facilities.

Here is an abstract:

At AIM4 in May last year I talked about my joint work with Andreas Abel
and Klaus Aehlig on Normalization by Evaluation for Martin-Löf Type Theory
with One Universe. A paper with the details behind this talk will be
presented at the upcoming MFPS-conference. In the present talk I will
explain a few of the subsequent developments. The MFPS-paper is based on a
version of Martin-Löf type theory with untyped conversion. However, the
official version of Martin-Löf type theory is based on a typed notion of
conversion, formalized as equality judgements, and the nbe-technique
applies equally well (even better) to this theory. Thierry got interested
in investigating this further, especially with the goal to get a nice
proof of the elusive property that Pi is one-to-one. As a consequence one
sho