[Agda] Re: 'Dummie' question - why records?

[Zhaohui Luo]

People in this thread may be interested in the following paper of mine on dependent record types

http://www.cs.rhul.ac.uk/home/zhaohui/DRT11.pdf
from where you can also find references to several related earlier papers on DRTs.  

Particulary relevant to some of the discussions in this thread is the discussion on the relationship between record types and Sigma-types in the above paper.
 
Best regards,
 
Zhaohui


-------------------------------------
Professor Zhaohui Luo 
Department of Computer Science 
Royal Holloway, University of London 
Email: zhaohui.luo at hotmail.co.uk
URL: www.cs.rhul.ac.uk/home/zhaohui/
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111026/63e8aeca/attachment.html