So, today Rob Simmons, Chris Martens, William Lovas and I (with help from Dan Licata) hosted a Twelf/Agda school. Since I typed for a few hours with Rob's normally-bound keys for Agda mode, I'm going to save my wrists and keep this post short. Basically, we showed a few basic encodings of addition in Agda and one in Twelf, proved a few things like commutativity, and generally treid to show off a bunch of the useful and interesting features these languages provide. I'll post the code later tonight.
Also, there appears to be a workshop paper about randomized decision trees which are differentially private; related to what I want to do but not quite the same because I suspect the organization of randomized trees will make difficult post-pruning without substantial information loss.
No comments:
Post a Comment