| ← Fun in Nottingham, February 2007 | Fun in York, November 2007 → |
Our third meeting was held on Thursday 17 May 2007, in West Cambridge, organised by Alan Mycroft and Peter Buchlovsky. Many thanks to Andrew Kennedy for proving that at Microsoft, there is such a thing as a free lunch. With about seventy in attendance and really interesting stuff from Andy, Joao, Ben and Tarmo, Fun seems to be making its mark.
Dinner was (you guessed it) curry, at the Maharajah, on Castle Hill. As ever, here's the receipt. Thanks to Axel Simon for the scan.
Roll up! Roll up! For all the FUN of the fair!
The "Fun in the afternoon" termly functional programming event takes place in Cambridge this Thursday.
We asked our admin about car parking. They say:
Parking is not that much of a problem here. If you only anticipate very few vehicles (less than 10) that would need to be parked, then the visitors car park [directly in front of our building] should cope. If however you need more than ten parking spaces then we could advise them to use the service entrance/Goods In area, and if push comes to shove, the roads around us do not have any yellow lines yet, so as a last resort parking on the roadway might suit. There is also lots of quiet-street parking on James Clerk Maxwell Road (the next turnoff from Madingley Road (A1303) in the towards-town direction, same side of road).
Microsoft are kindly providing a buffet lunch for those arriving for 12:30 (this is in the reception of the Microsoft Research building 100m behind (East of) the Computer Lab (turn left at our reception and go round the side of our building). First come first served!
Alan adds: We've asked for buffet lunch for 40, so... ... if you would like to partake of MSR's generous offer, then
| 12.00 - 14.00 | Lunch: bring your own, or... |
| 12.30 | ...come early and have a Microsoft buffet! |
| 14.00 - 15.00 | Baltic: Service Combinators for Farming Virtual Machines |
| Andy Gordon, Microsoft Research, Cambridge | |
| Andy's slides | |
| 15.00 - 15.30 | Coffee |
| 15.30 - 16.00 | Recounting the Rationals: Twice! |
| Joao Fernando Ferreira, University of Nottingham | |
| Joao's slides | |
| 16.00 - 16.30 | Why eager and lazy are not quite dual |
| Ben Rudiak-Gould, University of Cambridge | |
| 16.30 - 17.00 | Firmly antifounded |
| Tarmo Uustalu, Institute of Cybernetics, Tallinn | |
| Tarmo's slides |
Baltic: Service Combinators for Farming Virtual Machines
Andy Gordon,
Microsoft Research, Cambridge
We consider the problem of managing server farms largely automatically, in software. Automated management is gaining in importance with the widespread adoption of virtualization technologies, which allow multiple virtual machines per physical host. We consider the case where each server is service-oriented, in the sense that the services it provides, and the external services it depends upon, are explicitly described in metadata. We describe the design, implementation, and formal semantics of a library of combinators whose types record and respect server metadata. Our implementation consists of a typed functional script built with our combinators, in control of a Virtual Machine Monitor hosting a set of virtual machines. Our combinators support a range of operations including creation of virtual machines, their interconnection using typed endpoints, and the creation of intermediaries for tasks such as load balancing. Our combinators also allow provision and reconfiguration in response to events such as machine failures or spikes in demand. We describe a series of programming examples run on our implementation, based on existing server code for order processing, a typical data centre workload. To obtain a formal semantics for any script using our combinators, we provide an alternative implementation of our interface using a small concurrency library. Hence, the behaviour of the script plus our libraries can be interpreted within a statically typed process calculus. Assuming that server metadata is correct, a benefit of typing is that various server configuration errors are detected statically, rather than sometime during the execution of the script. [Based on joint work with Karthikeyan Bhargavan, Microsoft Research and Iman Narasamdya, University of Manchester]
Recounting the Rationals: Twice!
Joao Fernando Ferreira,
University of Nottingham
In this talk we present an algorithm that enables the rationals to be enumerated in two different ways. One way is known and is called Calkin-Wilf-Newman enumeration; the second is new and corresponds to a flattening of the Stern-Brocot tree of rationals. We show that both enumerations stem from the same simple algorithm. In this way, we construct a Stern-Brocot enumeration algorithm with the same time and space complexity as Calkin-Wilf-Newman enumeration.
Why eager and lazy are not quite dual
Ben Rudiak-Gould,
University of Cambridge
Writing down a denotational semantics for strict and non-strict ML is a tricky business: in particular, it is not always clear what should be lifted or why. We have previously shown how a simple continuation-based intermediate language is useful for compiling strict and non-strict languages to a single virtual machine (Haskell is Not Not ML, ESOP '06). In this talk I will show how the negation-based type system of this language can usefully model the habitation of types in ML and Haskell, and in two variations of Haskell semantics: Haskell without seq, and "dual Haskell" where code is represented by data and data by code.
Firmly antifounded
Tarmo Uustalu,
Institute of Cybernetics, Tallinn
Recursive coalgebras are a simple formulation of wellfounded recursion and termination. In an attempt to learn about antifounded recursion and productivity, we play with their dual concept. Since Set is not self-dual, this is not without surprises. (Joint work with Venanzio Capretta and Varmo Vene.)