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

[Peter Dybjer]

The slides from my talk is now on

http://www.cs.chalmers.se/~peterd/papers/nbe.html

where there is also some other stuff about nbe.

Cheers, Peter

P.S. Fredrik can you post it on the proglog-talk list too?

Peter Dybjer wrote:

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