I am a professor in the Computer Science and Engineering Department at Chalmers University of Technology.
ms (at) cs (dot) chalmers (dot) se
Andy Martin from IBM and John O'Leary from Intel are running HFL 2009 with ETAPS in York. HFL stands for Hardware Design and Functional Langauges. The programme for HFL 2009 has now been decided. It looks very stimulating. I will be there.
I am on the PC of the tenth Symposium on Trends in Fuctional Programming, which will be held in Slovakia from June 2-4, 2009. Here is the call for papers. I encourage you to submit. I will also lecture on the Central European Summer School on Functional Programming which will be held in the same place, immediately before TFP.It looks like a very interesting summer school indeed.
I was on the PC of the 2008 Haskell Symposium, which was in Victoria, British Columbia on Sept. 25th, 2008, just after the International Conference on Functional Programming.
I was on the PC of the International Workshop on Discrete Event Systems, 2008. This was held here at Chalmers, and was run by my colleagues at the Signals and Systems department. We held a session about SAT and its applications.A journal paper is now growing out of our tutorial paper on SAT and its applications.
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!
I am a founding member of the IFIP Working Group 2.8 on Functional Programming.