Programming in the Era of Cloud, Data and Devices, F# 3.0 Information Rich Programming

Advances in programming languages are placing powerful, programmatic problem-solving tools in the hands of analytical programmers, But programming today exhibits a voracious appetite for information, and, even though our languages are wonderfully interoperable, they are in many ways information sparse. There is always with an impedance mismatch between the inner world of the language and the outer world of known services and data sources. Fluency here can achieve wonders in simplifying the modern programming problem. At the same time, data in the web is transitioning from adhoc to professional services, with a range of access options from free to service-guaranteeed. This track will look at themes in data and services on the web, and the languages and techniques we can use to consume it.

Speaker Bios

I graduated from the Australian National University in 1993, and joined Microsoft Research in 1998. Before that I was a PhD. student at the University of Cambridge Computer Laboratory http://www.cl.cam.ac.uk. A while ago I spent three months at SRI http://www.csl.sri.com and a six month jaunt at Intel http://www.intel.com. Clearly my ultimate aim is to work for every multinational mega corporation in the computing game, so I’ll throw in links to IBM http://www.ibm.com, Sun http://www.sun.com and Compaq http://www.compaq.com for good measure. My research interests include the formal modeling of programming languages and abstract machines and techniques for the verification of their properties. Example machines include high level languages defined by operational semantics, stack machines such as the JVM, and hardware devices at various levels of abstraction. Typical properties include correctness (by correlating the machine against a higher-level specification) and type soundness (by proving the preservation of an appropriate invariant, which is implied by a statically checked condition). Typical techniques include model checking, automated reasoning, abstract interpretation and manual declarative proof declare/index.htm. Since joining MSR I’ve worked extensively with the COM+ team analyzing their code verification mechanism along with Andy Gordon.