The ICFP 2009 PC team will be in Portland next week, and PSU is holding a free one day functional programming workshop to conincide with the meeting: the ICFP PC Functional Programming Workshop. The program has talks from leading researchers in language design and functional programming:

• Algebra of Programming using Dependent Types. Shin-Cheng Mu (Academia Sinica)
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types.Lars Birkedal (IT University of Copenhagen)
• A Compiler on a Page.Kristoffer Rose (IBM Thomas J. Watson Research Center)
• A Proof Theory for Compilation.Atsushi Ohori (Tohoku University)
• Data Parallelism in Haskell.Manuel Chakravarty (University of New South Wales)
• Push-down control-flow analysis of higher-order programs. Matthew Might (University of Utah)
• Slicing It: indexed containers in Haskell.Conor McBride (University of Strathclyde)

The event is on the PSU campus. See the workshop home for directions.See you there!

The March 24th Galois Tech Talk was delivered by Aaron Tomb, titled “Fun with Dependent Types.”

• Date: Tuesday, March 24, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Here are Aaron’s slides. Further material on this topic can be found on Kenn Knowles’s site.Abstract: A number of dependently-typed programming languages exist, but many either restrict expressiveness or require extensive user input to deal with the undecidability of type checking. Languages such as Cayenne, lambda-H, and Sage have instead used a “best-effort” attempt to deal with this undecidability by attempting to type check programs, but potentially failing to prove valid programs type-correct.One powerful (and undecidable) form of dependent typing is based on what are variously known as contract types, refinement types, or predicate subtypes. The lambda-H language uses refinement types alone, and Sage includes them as part of a “pure” type system that uses the same syntax to describe both terms and types.An interesting recent result (by one of my friends from Santa Cruz) shows that while type checking for refinement types is undecidable, a form of type inference is decidable. It has the interesting property that if the input program is well-typed, then it has the inferred type. However, the algorithm does not determine whether the input program is, in fact, well-typed. Because it only decides one part of the type inference problem, the authors refer to it as “type reconstruction” instead.I will talk about refinement types, existing techniques for checking them, and the basics of decidable refinement type reconstruction.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Commercial Users of Functional Programming Workshop 2009:Functional Programming as a Means, Not an EndSponsored by SIGPLANCo-located with ICFP 2009Edinburgh, Scotland, 4 September 2009Galois is excited to promote this sixth annual event and encourages any interested in speaking at the workshop to send in a presentation proposal!  Whether you’d like to offer a talk yourself or you’d have someone in mind you’d like to nominate, please submit a proposal by 15 May 2009 via e-mail to francesco(at)erlang-consulting(dot)com or jim(dot)d(dot)grundy(at)intel(dot)com. Include a short description (approx. one page) of what you’d like to talk about or what you think your nominee should give a talk about.Do I have a presentation idea?If you use functional programming as a means rather than as an end (or could nominate someone who does), we invite you to offer to give a talk at the workshop. Talks are typically 25 minutes long but can be shorter and aim to inform participants about how functional programming plays out in real-world applications. Your talk does not need to be highly technical, and you do not need to submit a paper!What is the goal?The goal of the CUFP workshop is to act as a voice for users of functional programming and to support the increasing viability of functional programming in the commercial, governmental, and open-source space. The workshop is also designed to enable the formation and reinforcement of relationships that further the commercial use of functional programming.Tell me more!CUFP 2009 will last a full day and feature a keynote presentation from Bryan O’Sullivan, co-author of Real World Haskell. The program will also include a mix of presentations and discussion sessions varying over a wide range of topics.This will be the sixth CUFP;  for more information, including reports from attendees of previous events and video of recent talks, see the workshop web site: http://cufp.galois.com/.

The March 10th Galois Tech Talks was delivered by Don Stewart on “Specialising Generators for High-Performance Monte-Carlo Simulation in Haskell.”Here are the slides.

• Date: Tuesday, March 10, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: We address the tension between software generality and performance in the domain of simulations based on Monte-Carlo methods. We simultaneously achieve generality and high performance by a novel development methodology and software architecture centred around the concept of a specialising simulator generator. Our approach combines and extends methods from functional programming, generative programming, partial evaluation, and runtime code generation. We also show how to generate parallelised simulators.We evaluated our approach by implementing a simulator for advanced forms of polymerisation kinetics. We achieved unprecedented performance, making Monte-Carlo methods practically useful in an area that was previously dominated by deterministic PDE solvers. This is of high practical relevance, as Monte-Carlo simulations can provide detailed microscopic information that cannot be obtained with deterministic solvers.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

If you get IEEE Computer, check out the article on page 108 of the January, 2009 issue: Rosetta: Standardization at the System Level.  The author, Perry Alexander , is a professor at the University of Kansas.  Perry describes Rosetta, a language for designing and modeling systems.  The language is undergoing IEEE standardization, and there’s even a book describing the language.Perry collaborates with me and others at Galois, Inc. and has used Rosetta on one of our joint formal methods projects.

Don did an interview with Michael Wrinn and Aaron Tersteeg from Intel’s Multicore Software Development podcast about Haskell, multicore and parallel programming, and the use of functional programming at Galois and in industry in general. Listen to the full interview! (15 minutes).

This week’s tech talk will be Magnus Myreen from Cambridge talking about mechanically verified Lisp interpreters. It will be held at the irregular time of 2pm, Friday Nov 14.

This talk describes work on constructing verified interpreters for a small LISP-like language using the interactive theorem prover HOL4.  The LISP interpreters have been proved correct with respect to detailed x86, ARM and PowerPC processor models (written by Sarkar, Fox and Leroy). New techniques for expressing correctness of machine code were developed, as well as new techniques for proof-producing decompilation and compilation to/from HOL4 functions. A copying garbage collector (a Cheney collector) was verified and subsequent proofs were built upon its verified specification.

Don will be giving a talk SC’08 in Austin, Texas on Monday 17th November, as part of the Bridging Multicore’s Programmability Gap workshop (see the schedule here), talking about programming mainstream multicore systems with Haskell, now. Here’s the abstract,

Haskell is a general purpose, purely functional programming language. If you want to program a parallel machine, a purely functional language such as Haskell is a good choice: purity ensures the language is by-default safe for parallel execution, (whilst traditional imperative languages are by-default unsafe).This foundation has enabled Haskell to become something of a melting pot for high level approaches to concurrent and parallel programming, all available with an industrial strength compiler and language toolchain, available now for mainstream multicore programming.In this talk I will introduce the features Haskell provides for writing high level parallel and concurrent programs. In particular we’ll focus on lightweight semi-explicit parallelism using annotations to express parallelism opportunities. We’ll then describe mechanisms for explicitly parallel programs focusing on software transactional memory (STM) for shared memory communication. Finally, we’ll look at how Haskell’s nested data parallelism allows programmers to use rich data types in data parallel programs which are automatically transformed into flat data parallel versions for efficient execution on multi-core processors.

See Simon Peyton-Jones and Satnam Singh’s recent tutorial for more background on multicore Haskell, on which this talk is based.

A special Galois tech talk next week, with Slava Pestov talking aboutthe Factor programming language, environment, and implementation.

Logistics

• Thursday Oct 30, 2008, 10.30 – 11.30

Abstract

Factor is a programming language which has been in development for a little over 5 years. Factor is influenced by Forth, Lisp, Smalltalk. Factor takes the best ideas from Forth — simplicity, short, succint, code, emphasis on interactive testing, and meta-programming. Factor also brings modern high-level language features such as garbage collection, object orientation and functional programming familiar to users of languages such as Lisp, Smalltalk and Python. Finally, recognizing that no programming language is an island, Factor is portable, ships with a full-featured standard library, deploys stand-alone binaries, and interoperates with C and Objective-C.In this talk, I will give the rationale for Factor’s creation, present an overview of the language, and show how Factor can be used to solve real-world problems with a minimum of fuss. At the same time, I will emphasize Factor’s extensible syntax, meta-programming and reflection capabilities, and show that these features, which are unheard of in the world of mainstream programming languages, make programs easier to write, more robust, and fun.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities.

Tuesday’s tech talk was a special treat, with Jason Dagit dropping by to talk about using GADTs to clean up the darcs patch theory implementation. (.pdf slides).Logistics

• Tuesday, Oct 14, 2008, 10.30 – 11.30

Abstract

Darcs is based on a data model, known as Patch Theory, that sets it apart from other version control systems. The power of this data model is that it allows Darcs to manage significant complexity with a relatively straightforward user interface.We show that Generalized Algebraic Data Types (GADTs) can be used to express several fundamental invariants and properties derived from Patch Theory. This gives our compiler, GHC, a way to statically enforce our adherence to the essential rules of our data model.Finally, we examine how these techniques can improve the quality of the darcs codebase in practice.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities.