Chalmers Functional Programming Workshop 2009
- Tuesday, June 16.
- 9.00 - 16.30
- Ascom, student union building
Emil Axelsson, Niklas Broberg, JP Bernardy, Magnus Björk, Karina Bunyik, Koen Claessen, Patrik Jansson, Ann Lillieström, Kálmán Karch, Ulf Norell, Nick Smallbone, Josef Svenningsson, Hans Svensson, Joel Svensson, Wouter Swierstra
|09.00-09.15||Welcome + presentation|
|Session 1: Chair: Koen|
|09.15-09.55||Wouter||Swierstra||Talk: Chalk - a tool for hardware description|
|09.55-10.05||Joel||Svensson||Stat.Rep.: Obsidian - an embedded language for GPGPU programming|
|10.05-10.15||Ulf||Norell||Stat.Rep.: Proving laws of arithmetic in Agda|
|Session 2: Chair: Wouter|
|10.45-11.25||Koen||Claessen||Talk: Showing and Shrinking Functions|
|11.25-11.35||Ann||Lillieström||Stat.Rep.: Infinox - when are there no finite models?|
|11.35-12.15||Emil||Axelsson||Talk: An embedded language for digital signal processing|
|Karina||Bunyik||(co-presenter with Emil Axelsson)|
|Kálmán||Karch||(co-presenter with Emil Axelsson)|
|12.15-13.15||Lunch at Hyllan|
|Session 3: Chair: Emil|
|13.15-13.25||Hans||Svensson||Stat.Rep.: Erlang QuickCheck for Rose/RT code at Ericsson RBS|
|13.25-13.35||Magnus||Björk||Stat.Rep.: Qualitative Study of SAT Encodeing Techniques|
|13.35-14.15||Patrik||Jansson||Talk: Playing with type classes|
|14.25-14.35||Nick||Smallbone||Stat.Rep.: A logic for QuickCheck properties|
|Session 4: Chair: Hans|
|15.15-15.30||Anders||Persson||Stat.Rep.: DSL for hard real time SW|
|15.30-15.45||Josef||Svenningsson||Stat.Rep.: Shortcut Fusion and Tuples|
|15.45-16.00||Niklas||Broberg||Stat.Rep.: Google Summer of Code on haskell-src-exts|
Stat.Rep. = Status Report
- Chalk - a tool for hardware description
- Wouter Swierstra
- In this talk, I'd like to outline the ideas underlying Chalk, a domain specific embedded language for hardware design, on which Koen, Mary, and I have been working. Chalk draws inspiration from Hawk, a previous DSL for hardware description in Haskell. The embedding of Hawk into Haskell is very shallow: the only thing you can do with Hawk circuits is simulate them. Lava, on the other hand, takes a different approach. By giving a deep embedding of the DSL there are various analyses and interpretations you can give to Lava circuits. Chalk aims to sit in-between these two languages: exposing Hawk's high-level combinators for circuit description to the user, while still making the embedding deep enough to analyse the resulting circuits.
- Showing and Shrinking Functions
- Koen Lindström Claessen
- In QuickCheck, you can quantify over functions, but when a counter example is found, the functions can neither be shown nor shrunk. I will show a technique that we can use to do both of these. It turns out you cannot show a function unless you shrink it first!
- An embedded language for digital signal processing
- Emil Axelsson, Karina Bunyik, Kálmán Karch
- We present a domain-specific language for digital signal processing (DSP) embedded in Haskell. High-level, efficient descriptions are achieved by the use of "symbolic vectors", which support efficient list-like operations and loop fusion. We will show the important aspects of the implementation, and demonstrate its usefulness on some important DSP algorithms.
- Providing Integrity Policies as a Library in Haskell
- Albert Diserholt (Master student)
- Confidentiality policies refer to preserving secrecy of data, while integrity policies seek to prevent accidental or malicious destruction of information. Information-flow techniques have been developed over the years to preserve confidentiality, i.e. to prevent secret data being leaked into public channels. Some integrity policies can be seen as dual to confidentiality: meaningful and correct data should not be affected by corrupted or untrusted data. However, this notion of integrity is weaker than the one needed in practice. For example, it is often the case that integrity policies involve some notion of who can access the information (i.e. access control) or some invariants on the processed data. Clearly, these kind of integrity policies cannot be expressed as dual to confidentiality. Rather than producing a new language from scratch, information-flow security can be provided as a library. There exists libraries to preserve confidentiality of data for Haskell programs. However, they do not consider integrity policies. This talk presents some preliminaries ideas regarding how to extend the monadic library developed by Russo et. al.  in order to include integrity policies. The talk is based on a work-in-progress. Bibliography:  A Library for Light-weight Information-Flow Security in Haskell, with Koen Claessen and John Hughes. In Proceedings of the ACM SIGPLAN 2008 Haskell Symposium, Victoria, British Columbia, Canada, September 2008.
- Playing with type classes
- Patrik Jansson
- While working on translating a Haskell "executable specification" to generic C++ code we have learnt a few things about (multi-parameter) type classes and associated types.
- Shortcut Fusion and Tuples
- Josef Svenningsson
- Recursive functions which return tuples are hard to compile efficiently. I show how in certain circumstances the tuples can be removed completely, using techniques based on shortcut fusion.
- Ungsbakad kolja med räkfräs, citronhollandaise och färsk potatis
- Kalvgrikassé med primörer, madeirasås samt färsk potatis
Mails and information
This is a reminder about the call for presentations below and a call for "registration" (incl. dietary requirements for the lunch) at the following doodle.
I have added those who have already indicated that they can come - please check that you're data is correct. Note that there are links for editing or removing an entry at the bottom of the page.
The workshop will take place in the room "Ascom" in the student union building  with the following rough schedule:
|12.15||lunch at "Hyllan"|
|13.15||afternoon session start|
The length of the pres. slots depend on the number of talk submissions we get, so prepare to be interrupted;-) Style-wise I'd like all presentations to maximise the interaction with the other participants - perhaps with a few "exercises" to solve or a demo or something else in the style of "a workshop / a summer school / teamwork" rather than just "lecture". I want pdf-files of all the presentations by Monday evening (20.00).
The Functional Programming research group of the SET division is organizing an informal one-day workshop next Tuesday (20090616). The aim is for Chalmers researchers who are interested in functional programming to meet, interact and discuss, and to comment on each others work.
We are now soliciting presentation proposals for this workshop (see below), both from members of our own group as well as people from other groups and divisions. In the case of overwhelming interest, a small program committee will select what presentations will be held. (We will prioritize presentations on core functional programming and proposals by members of our research group.) It is allowed to submit more than one proposal.
CHALMERS FUNCTIONAL PROGRAMMING WORKSHOP
- Tuesday, June 16.
- 9.00 - 16.30
- Ascom, student union building
CALL FOR PRESENTATIONS
You can submit a presentation proposal. Please include:
- a title
- a short abstract (at most two paragraphs)
- your co-authors
- if you have any time constraints on that day
We welcome work in progress, crazy ideas, presentations that generate discussions, etc. and prefer that over well-established, already published work.
Submission deadline: Sunday, June 14. Submit by sending an e-mail to me (patrikj at chalmers dot se) containing the above information.
TOPICS OF INTEREST
- applications of functional programming
- functional programming techniques
- functional programming tools
- test and verification of functional programs
- other common interests shared by members of the FP group
Participation to the workshop will be restricted to (1) presenters, and (2) members of the Functional Programming group.