[Haskell] Fun in the Afternoon (Cambridge, Thursday)

[Conor McBride]

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.