Relayed from Alan Mycroft: The "Fun in the afternoon" termly functional programming event takes place in Cambridge this thurday. For more details (including travel) see: http://sneezy.cs.nott.ac.uk/fun/ STOP PRESS: 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! For those of us coming later, there will be a room in the Computer Laboratory to buy or eat our own sandwiches. Programme: 2.00pm Andy Gordon (MSR, Cambridge) Baltic: Service Combinators for Farming Virtual Machines 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] ========= 3.00 coffee ========= 3.30 Joao Fernando Ferreira, University of Nottingham Recounting the Rationals: Twice! 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. ========= 4.00 Ben Rudiak-Gould, University of Cambridge Why eager and lazy are not quite dual 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. ========= 4.30 Tarmo Uustalu, Institute of Cybernetics, Tallinn Firmly antifounded 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.) See you for Fun on Thursday... Alan This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.