On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep
WG211/M19Carette
From WG 2.11
When a programming language doesn't have the features you want, WG2.11 people always do the same thing: implement a PL on top of them to get the job done.
Here we find Agda's facilities for creating and manipulating theories (whether as records or modules) wanting, so we set about to fix the problem. First, by creating a completely undisciplined prototype to hash out the requirements, then a second version will hopefully emerge that is 'sensible'.
(joint work with Musa Al-hassy and Wolfram Kahl)
