We are having the pleasure to host Peter Thiemann from the University of Freiburg at UNSW at the moment. His many contributions span the areas of functional programming, type systems, static analysis, program specialisation, and web programming.

Coming Monday (19 March), Peter will give a presentation at the School of Computer Science and Engineering (CSE) of the University of New South Wales. The details are as follows.

 

Time: 19 March 2012 (Monday), 11AM

Location: CSE Seminar room (K17_113), Level 1, CSE Building (K17)

 

Title: A Calculus for Gradual Access Control

Speaker: Peter Thiemann (University of Freiburg, Germany)

Abstract 

Many client-side Web applications are composed of script fragments that are independently downloaded from the Web. A recurring problem in that scenario is the need to impose an access control policy on the execution of a downloaded script. No script should be able to compromise the state of the base application, that is, it should neither access nor change sensitive data, which can be private data of the application, sensitive state of the browser, or a part of the DOM that is not explicitly assigned to it.

To address this situation, we want to construct a browser-embedded facility that regulates access control according to directives in a trusted program fragment. The calculus for gradual access control is the foundation of this facility. It incorporates a component that performs dynamic access control according to the directives. It also incorporates a static component that enables the system to omit the dynamic checks if it can prove them unnecessary. The two components are tightly connected by a gradual typing approach.

Bio

Peter Thiemann obtained his diploma in computer science in 1987 at the Technical University of Aachen, Germany. He graduated in 1991 at the University of Tübingen, Germany, where worked as a research and teaching assistent until 1997. In 1998, he was a lecturer in Computer Science at the University of Nottingham, England. Since 1999 he is a professor at the computer science department of the University of Freiburg, Germany, where he leads the programming languages group.

His research interests comprise theory and practice of modern programming languages, in particular program analysis, compiler construction, and program specialization for functional programming languages. The focus of his current research is static and dynamic program analysis for scripting languages.

Last year, we spent a lot of energy on reducing the memory consumption of vectorised Data Parallel Haskell (DPH) programs that use large shared data structures. This work was driven by an implementation of the Barnes-Hut algorithm in DPH. Ben produced an illustrative video animating an n-body simulation with his Gloss library. The video is part of his blog article Vectorisation without Replication in Data Parallel Haskell, where he explains the performance of our new DPH array library in comparison to our old library and a purely sequential implementation of Barnes-Hut based on Data.Vector.

Thanks to NICTA, John Launchbury will be in Sydney next week. He contributed in many ways to the development of the Haskell programming language and provided practical proof of the benefits of functional programming and formal methods by founding and leading the company Galois, Inc.

On Friday (20 January), John will give a presentation at the School of Computer Science and Engineering (CSE) of the University of New South Wales. The details are as follows.

 

Time: 20 January 2012 (Friday), 10.30AM

Location: CSE Seminar room (K17_113), Level 1, CSE Building (K17)

 

Title: A Snapshot on Secure Computation

Speaker: John Launchbury (Galois, Inc.)

Abstract

There is growing interest in performing computation on encrypted data, partly motivated by the challenges of cloud computing. As we lose control of the location of our data, we still want to retain control of the confidentiality and/or integrity of our data. If we could encrypt our data (either for confidentiality, or for integrity) and then have the cloud operators perform computations on the data in the encrypted form, then we may have the best of both worlds: the cloud supplies storage and computational resources, while the encryption provides guarantees about what happens to the data.

Recent theoretical breakthroughs in homormorphic encryption have raised the possibility of this working in practice, though there are very many challenging practical considerations to overcome first. In the meantime, a simpler method of secure shared computation is approaching practicality---the main limiting factor is the network communication required. The main weakness of sharing schemes is that they rely on the fairly weak security model of "honest but curious", though there are newer techniques to weaken this assumption.

In this talk we describe the current state of the art, and provide some specific insights into how to build plausibly efficient algorithms for shared computation.

Bio

Dr. John Launchbury is Chief Scientist of Galois, Inc. John founded Galois in 1999 to address challenges in Information Assurance through the application of Functional Programming and Formal Methods. Under his leadership, formerly as CEO, the company has grown strongly, successfully winning and delivering on multiple contracts for more than a decade. Prior to founding Galois, John was a full professor in Computer Science and Engineering at the Oregon Graduate Institute School of Science and Engineering at OHSU. John received First Class Honors in Mathematics from Oxford University in 1985. He holds a Ph.D. in Computing Science from University of Glasgow and won the British Computer Society's distinguished dissertation prize. In 2010, John was inducted as a Fellow of the Association for Computing Machinery (ACM) for his contributions to functional programming.

 

As part of YOW! 2011 (the Australian Software Developer Conference), Simon Peyton Jones and John Hughes will be in Sydney on the 7th and 8th of December 2011. On the evening of the 7th, they will appear at the YOW! Night Sydney.

On Thursday (8 December), John and Simon will give two presentations at the School of Computer Science and Engineering (CSE) of the University of New South Wales. The details are as follows.

Time: 8 December 2011, 10AM

Location: CSE Seminar room (K17_113), Level 1, CSE Building (K17)

 

 

Talk #1

Title: Accelerating race condition detection through procrastination

Speaker: John Hughes (Chalmers University & Quviq AB)

Abstract

Race conditions are notoriously frustrating to find, and good tools can help. The main difficulty is reliably provoking the race condition. In previous work we presented a randomising scheduler for Erlang that helps with this task.

In a language without pervasive shared mutable state, such as Erlang, performing scheduling decisions at random uncovers race conditions surprisingly well. However, it is not always enough. We describe a technique, procrastination, that aims to provoke race conditions more often than by random scheduling alone. It works by running the program and looking for pairs of events that might interfere, such as two message sends to the same process. Having found such a pair of events, we re-run the program but try to provoke a race condition by reversing the order of the two events.

We apply our technique to a piece of industrial Erlang code. Compared to random scheduling alone, procrastination allows us to find minimal failing test cases more reliably and more quickly.

John Hughes

John Hughes has worked with functional programming since 1980, was one of the designers of Haskell, and has been heavily involved with Erlang in recent years. In 2000 he and Koen Claessen published the first version of QuickCheck, a software testing tool which recently won the ACM SIGPLAN award for Most Influential Paper from ICFP in that year. He has focussed more and more on testing since then, co-founding Quviq AB in 2006 to market a commercial version of QuickCheck. He is currently both a Professor at Chalmers University, Sweden, and CEO of Quviq AB.

 

Talk #2

Title: Termination Combinators Forever

Speaker: Simon Peyton Jones (Microsoft Research)

Abstract

Nobody wants their compiler, or theorem prover, to go into an infinite loop, but making sure that never happens usually means applying some over-conservative heuristic like “never unfold a recursive function”. Approaches like that don’t work at all when you are doing partial evaluation or supercompilation, which fundamentally depend on inlining recursive functions. 

What we need is an online termination test. That is easier said than done; it is easy to make a mistake. In this talk I’ll describe a new combinator library that lets you build complex termination tests by combining simpler ones, while guaranteeing that that the result really is a termination test. The library elegantly encapsulates some clever mathematical ideas on well-quasi orders the cunning details are hidden from the customer.

I’ll use Haskell as the language of exposition, but you don’t need to be a Haskell guru to understand it, and the library would work equally well in other languages.

Simon Peyton Jones

Simon Peyton Jones, MA, MBCS, CEng, graduated from Trinity College Cambridge in 1980. After two years in industry, he spent seven years as a lecturer at University College London, and nine years as a professor at Glasgow University, before moving to Microsoft Research (Cambridge) in 1998.

His main research interest is in functional programming languages, their implementation, and their application. He has led a succession of research projects focused around the design and implementation of production-quality functional-language systems for both uniprocessors and parallel machines. He was a key contributor to the design of the now-standard functional language Haskell, and is the lead designer of the widely-used Glasgow Haskell Compiler (GHC). He has written two textbooks about the implementation of functional languages.

More generally, he is interested in language design, rich type systems, software component architectures, compiler technology, code generation, runtime systems, virtual machines, and garbage collection. He is particularly motivated by direct use of principled theory to practical language design and implementation — that's one reason he loves functional programming so much.

 

As an add-on to the just released GHC 7.2.1, Ben just uploaded the Data Parallel Haskell packages (version 0.5) to Hackage. This version is still largely a technology preview and not a production-ready system. Nevertheless, it is significantly more robust than previous versions, especially for programs with a statically fixed depth of nesting of parallelism. For further information on how to install and use Data Parallel Haskell (DPH), see the DPH documentation.

We just released version 2.0.0.1 of the Repa array library for Haskell, which includes Ben's recent work on high-performance, parallel stencil computations. The work on stencil computations is described in detail in a draft paper entitled 
Efficient Parallel Stencil Convolution in Haskell. Be sure to check out Ben's screencast of a real-time edge detection application, written in Objective-C and Haskell, using the new Repa library. For more details, see Ben's blog post.

Simon Peyton Jones recently gave a talk on parallel programming in Haskell at Functional Programming eXchange 2011. It provides a comprehensive overview of the state of the art of parallel programming in Haskell. It covers Software Transactional Memory, Erlang-style communicating processes, parallel strategies as well as our Data Parallel Haskell, Repa, and Accelerate projects. Watch the video.

David Terei wrote a post for the LLVM project blog summarising the motivation and experiences from his Honours project.  The blog post contains a nice summary of the GHC LLVM backend project and quotes some new benchmark results.

We released the first version of Repa — our parallel array library for Haskell described in the paper Regular, shape-polymorphic, parallel arrays in Haskell.