Mary Sheeran

I am a professor in the Computer Science and Engineering Department at Chalmers University of Technology.

How to reach me

Postal address: Computer Science and Engineering Dept. (D&IT)
Chalmers University of Technology
SE-412 96 Göteborg
SWEDEN
Visiting address: D&IT building, room 5466
Phone: (+46)-31-772 10 13
Fax: (+46)-31-16 56 55
E-Mail: ms (at) cs (dot) chalmers (dot) se

celtic bar

Update: returning to normal

After two successful eye operations during August, I returned to work around the beginning of October. It is surpisingly hard to get going again afer a five month absence. 2010 will be largely devoted to the Feldspar project with Ericsson, We are developing a domain specific language for Digital Signal Processing and Emil Axelsson and our colleagues at ELTE Budapest have been doing a great job with this in my absence. Ericsson has increased their funding of the project so that Emil and I will be joined by Josef Svenningsson as postdoc on the project in 12010. Also, my Ericsson colleague Anders Persson will become an industrial doctoral student on the project, as we obtained funding from the Swedish basic research agency (VR) for this. I have funding from another funding agency (SSF) to spend 80% of my time on this project for the first half of next year, and 50% for the remainder of the year. We are currently writing some papers about Feldspar. Ericsson has also realeased the first version open source. In addition, the Functional Programming group at Chalmers has received a large grant for work on Domain Specific Languages from VR. So we're all set to do great things in 2010. We will shortly be advertising a PhD position and a 4 year post-doctoral research position in the Functional Programming group. Watch this space.

Reading

As many of you know, I have been interested in parallel prefix networks for a long time. I have written down most of what I know in a paper that I submitted to JFP. I have also made it into a technical report: Functional and dynamic programming in the design of parallel prefix networks by Mary Sheeran, TR-2009:12. It's cool stuff. I would be grateful for any comments or suggestions.

Conferences and Workshops

The International Conference on Formal Methods in Computer Aided Design of Electronic Circuits (FMCAD 2009) was held in Austin, Texas, from November 15 to 18, 2009. As usual, I really enjoyed it.I like the fact that participation is half from industry and half from academia. FMCAD is an excellent conference, and it just keeps getting better. You will find that at least since FMCAD 2006, FMCAD conference pages include (under "Advnace Program") slides from both ordinary presentations and invited talks and tutorials. There are many gems among these talks, and the collection is a very useful resource for the community. I have been to every single FMCAD conference, and really enjoy the fact that the community is made up (roughly equally) of both of academics and of researchers and practitioners from industry. I chaired FMCAD along with Jason Baumgartner from IBM in 2007, and am now on the steering committee for the conference. If you have any ideas or suggestions for how to improve the conference, please let me know.

I have been asked to join the PC of the workshop on Commercial Users of Functional Programming for 2010. I am looking around for interesting talks. Please get in touch if you have one to suggest.

Research

My research interests are in functional programming, and particularly its application to hardware description and verification. Until recently, I was part of the Formal Methods group at Chalmers, but recently Koen Claessen, John Hughes and I decided to reform the Functional Programming Group. A major emphasis in the group is on Domain Specific Embedded Languages in the functional programming language Haskell. We have developed Lava for hardware design at the gate or netlists level, Wired for layout-aware hardware design and QuickCheck for specification-guided random testing of software. Recently, we have begun to investigate data-parallel programming for Graphics Processing Units (GPUs) as we are convinced that it is vital to find better ways to program parallel machines. In similar vein, we are talking to Ericsson about a Domain Specific Language for Digital Signal Processing. We also have a strong interest in automated reasoning, from SAT solvers and their applications to First Order Logic Theorem Proving and related topics.

One of my doctoral students, Niklas Een, successfully defended his thesis on February 8 2005. You might want to read his thesis and then download MiniSat. Together with the SatElite preprocessor, MiniSat won all three industrial categories in the SAT 2005 competition. So this is world-leading work that is freely available and is going to be widely used. Niklas now works at Cadence Berkeley Labs. He continues to work closely with Niklas Sörensson. Other students who have completed their theses and now work in industry are Per Bjesse (now at Synopsys in Portland ) and Jan-Willem Roorda (now at Fenix-DA in Eindhoven). Magnus Björk, who worked on an extension of Stålmarck's method to first order logic, defended his doctoral thesis on May 11, 2006. After a year in Oxford working with Tom Melham and Carl Seger on STE and abstraction, he is back at Chalmers working on a project investigating the inclusion of formal verification in the hardware design flow at Saab Space here in Göteborg.

Emil Axelsson has worked on Wired (see below). Emil got his lic. in May 2006, and defended his PhD thesis on Sept. 9, 2008. The second half of the thesis documents his work on the most recent version of the Wired system, and is extremely elegant. This work was funded by an Intel-custom grant from the Semiconductor Research Corporation. Emil will work, during 2009, on a project with Ericsson to develop a domain specific language for DSP algorithm design. I am also co-supervisor to Eva Suci in Bergen.

I now have a new student, Joel Svensson, working on programming methods for Graphics Processing Units (GPUs). Koen is co-supervisor. We are investigating whether the structural hardware design methods based on connection patterns that we developed for Lava (and even as far back as my work on muFP and Ruby) are also useful in this parallel programming context. It is looking good so far, and we are having fun. Joel has christened the new language Obdidian.

Here is my FMCAD'04 paper on generating fast multipliers using clever circuits. Copyright Springer Verlag. Clever circuits is a technical term :) My paper definitely added to the variety at this year's FMCAD. In June 2004, I talked about this work, and about my view of the use of a functional language in hardware design, at Intel Strategic CAD Labs. So here are the powerpoint slides of a presentation on functional languages and clever circuits. Here is the shorter talk that I gave at FMCAD'04. The circuit descriptions have become more beautiful.

At DCC 2004, Emil Axelsson presented the work that he, Koen Claessen and I have been doing on Wired, a language that takes account of the wires in circuits, in order to get a handle on non-functional properties like timing and power consumption. Our paper on Wired from CHARME 2005 is the first real publication on the topic. Since then, Matthew Naylor from York has visited us and introduced us to his own special brand of functional logic prgramming (but still embedded in Haskell). This formed the basis of a relational version of Lava and of a new Wired implementation. Finally, though, Emil used neat knot-tying functional programming techniques to make the final version of Wired. (See his thesis, which will appear here after the PhD defence on Sept. 9.) We had Intel-custom funding from the Semiconductor Research Corporation for this work. We have also benefitted from a donation of equipment from Intel. We find the contact with Intel Strategic CAD Labs (SCL) to be extremely stimulating. Recently, we benefitted from a three month visit by Emily Shriver from Intel (on what is called an externship, an interesting experiment in industrial-academic relations that Intel SCL has initiated).

At CHARME'03, I presented a paper about describing and analysing circuits that are almost regular. Copyright Springer Verlag. This work on clever circuits is funded by Vetenskapsrådet, the Swedish Research Council. When combined with the ideas in Wired and in Lava, the method is a very promising approach to the design of fast data-paths.

In November 2003, I gave an invited talk at the Nordic Workshop on Programming Theory (NWPT'03). I talked about my approach to describing and reasoning about sorting networks, and here are the slides.

Koen Claessen, Satnam Singh and I had a paper about designing and verifying a sorter core in Lava at CHARME'01. Copyright Springer Verlag.

At FMCAD 2000, Satnam Singh and I presented a paper about safety property checking using induction and a SAT solver. Copyright Springer Verlag. The main idea in the paper is due to Gunnar Stålmarck, though it also presents my non-standard way of thinking about the problem, and possible extensions. More work needs to be done in this area, to find good ways to include stronger constraints than the original "all states different". Many reported implementations are overly naive.

Lava embodies our ideas about hardware design and verification at the netlist (generator) level. You might want to start by reading the Lava tutorial. It is looking a bit long in the tooth now, and I hope to revise it in time for the next version of my course on hardware description and verification. Note that Lava is now available on Hackage. The plan is also to release Wired.

With Gunnar Stålmarck, I have written a longer version of our tutorial paper on Stålmarck's method of proof for propositional logic. The paper has now appeared in the journal Formal Methods in System Design, January 2000 issue.

Puzzling Permutations is a short paper that looks at how to describe and reason about multistage interconnection networks. It also poses a puzzle, which I myself have not so far been able to solve. The paper was presented at the Glasgow Functional Programming Workshop, 1996. I am leaving it on my home page in the hope that someone will solve the puzzle. I recently discovered that someone has solved this open problem! I have not got around to reading the paper yet. I will put some info. here once I have read it.Well, I never got around to reading the paper. But now I have discovered that the proof in it has been refuted. So the problem is still open. I am not sure it is good that I know that!

Teaching

A course on Hardware description and verification.

Other activities

I am a founding member of the IFIP Working Group 2.8 on Functional Programming.