[Agda] Marratech talk Wednesday 4 April 9.15 am Swedish time

[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:
>  
>
Some of the abstract was cut off last time. Here is a complete one (but 
shorter).

Abstract:
I will give an overview of some ideas on normalization by evaluation for 
Martin-Löf type theory which Andreas Abel, Thierry Coquand, and I have 
worked on together recently. I will in particular discuss an algorithm 
which is closer to Agda's and how it can be explained using normal forms 
in higher order abstract syntax. I will also give an introduction to 
categories with families and an algebraic formulation of Martin-Löf type 
theory, and motivate why our next version of normalization by evaluation 
will be using this formulation.

Peter