Galois › Blog » Functional Programming

Entries in the “Functional Programming” category

Tech Talk: An Introduction to Communicating Haskell Processes

March 10th, 2010 by Iavor S. Diatchki

Please note the unusual time-slot for this talk!

Details:

Title: An Introduction to Communicating Haskell Processes
Presenter: Neil Brown
Date: Monday, 15 March 2010
Time: 10:30am
Location: Galois Inc.
421 SW 6th Ave. Suite 300, Portland, OR, USA
(3rd floor of the Commonwealth building)

Abstract: Haskell is an excellent language for combining the power of functional programming with imperative constructs. This characteristic led to the development of the Communicating Haskell Processes (CHP) libraries, which support imperative synchronous message-passing in Haskell. The core ‘chp’ library provides basic message-passing, concurrency and choice, as well as integrated support for tracing. The ‘chp-plus’ library provides higher-level features such as process composition operators and behaviour combinators. This talk provides an introduction to the two libraries and the programming style they engender — as well as a brief look at the formal semantics underlying the libraries.

Bio: Neil Brown is a software researcher from the University of Kent in the UK. After graduating he worked for several years as a machine learning researcher in industry at QinetiQ, before returning to university to undertake his PhD. He started out writing a Haskell-based compiler for synchronous message-passing languages, and ended up programming some synchronous message-passing libraries for Haskell itself. As well as these CHP libraries, he also developed the Progression benchmark-graphing library for Haskell. More detail on both projects can be found on his blog.

Posted in Functional Programming, Haskell, Open Source, Tech Talks | Comments (1)

Tech Talk: Introduction to Aarne Ranta’s GF, the Grammatical Framework

February 11th, 2010 by Lee Pike

The talk will be presented by Iavor Diatchki on Tuesday, February 16th, at 10:30am.

(slides)
Abstract: The Grammatical Framework (created by Aarne Ranta) is a programming language for multilingual grammar applications. It may be seen in a number of different ways:

as a special-purpose language for grammars, like YACC or Happy, but not restricted to programming languages;
as a functional language, like Haskell or SML, but specialized to grammar writing;
as a logical framework, like Agda or Coq, but equipped with concrete syntax in addition to logic;
as a natural language processing framework, like LKB, or Regulus, but based on functional programming and type theory.

This talk is an introduction to GF’s basic concepts by example. We will look at how to define the meaning and syntax of a language, perform simple translations, define semantic properties, and how to use GF together with another language such as Haskell.

Bio: Iavor Diatchki is a R&D Engineer at Galois, Inc. with a Ph.D. from the Oregon Graduate Institute.

Details:

Date: February 16th, 2010, Tuesday
Time: 10:30am
Location: Galois Inc., 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth building)

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.

Posted in Community, Functional Programming, Haskell, Tech Talks | Comments (2)

Tech Talk: An Introduction to the Maude Formal Tool Environment

January 29th, 2010 by Iavor S. Diatchki

The talk will be presented by Joe Hendrix on Tuesday, February 2nd, at 10:30am. (slides)

Abstract: There is a great deal of interest today in developing multi-purpose environments that combine declarative programming, with specification languages and useful automated analysis techniques. In this talk, I will survey one such an environment: the Maude system. I will start by describing how to program in Maude with a focus on its support for rewriting modulo axioms. After some examples, I will also survey some of the different analysis tools developed on top of the Maude system —- including the model checker, inductive theorem prover, and an extension to the core language for modeling systems that operate in real-time.

Details:

Date: February 2nd, 2010, Tuesday
Time: 10:30am
Location: Galois Inc., 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth building)

Posted in Formal Methods, Functional Programming, Tech Talks | Comments (0)

Tech Talk: A Scalable I/O Manager for GHC

January 20th, 2010 by Iavor S. Diatchki

The talk will be presented by Johan Tibell on Friday, January 29th, at 1:30pm.

Slides are available (also on Slideshare and Scribd).

Abstract: The Glasgow Haskell Compiler supports extraordinarily cheap threads. These are implemented using a two-level model, with threads scheduled across a set of OS-level threads. Since the lightweight threads can’t afford to block when performing I/O operations, when a Haskell program starts, it runs an I/O manager thread whose job is to notify other threads when they can safely perform I/O.

The I/O manager manages its file descriptors using the select system call. While select performs well for a small number of file descriptors, it doesn’t scale to a large number of concurrent clients, making GHC less attractive for use in large-scale server development.

This talk will describe a new, more scalable I/O manager that’s currently under development and that hopefully will replace the current I/O manager in a future release of GHC.

Details:

Date: January 29th, 2010, Friday
Time: 1:30pm
Location: Galois Inc., 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth building)

Bio: Johan Tibell is a Software Engineer at Google Inc. He received a M.S. in Software Engineering from the Chalmers University of Technology, Sweden, in 2007.

Posted in Functional Programming, Haskell, Tech Talks | Comments (0)

GHC Nominated for Programming Language Award

January 6th, 2010 by john

ACM SIGPLAN recently announced a new award:

The SIGPLAN Programming Languages Software Award is awarded to an institution or individual(s) to recognize the development a software system that has had a significant impact on programming language research, implementations, and tools. The impact may be reflected in the wide-spread adoption of the system or its underlying concepts by the wider programming language community either in research projects, in the open-source community, or commercially. The award includes a prize of $2,500.

I think that GHC (Glasgow Haskell Compiler) and the two Simons (Peyton Jones and Marlow) are prime candidates for this. So, being careful to stay within the 500 word limit, I submitted a nomination statement for GHC as follows:

For the last decade, Haskell has been at the center of the most exciting innovations within programming languages, with work on software transactional memory, generalized algebraic data types, rank-N polymorphism, monads, multi-parameter type classes, embedded domain-specific languages, property-based testing, data parallelism, thread-profiling, and so on, generating hundreds of research papers from many diverse research groups.

GHC, the Glasgow Haskell Compiler, is the vehicle that made this research possible.

It is hard to explore radical ideas on real systems, yet the GHC team created a flexible platform that allows other researchers to explore the implications of their ideas and to test whether they really work in the large. From the first beta release in 1991, GHC emphasized collaboration and open “bazaar” style development, as opposed to the “cathedral” development of most of its contemporaries. GHC was open source even before Linux made open source cool. GHC has continued in the same vein, now listing over 60 contributors to the codebase.

In those early days, efficient compilation of a higher-order, allocation-rich, lazy functional language seemed to be a pipe dream. Yet GHC has risen to be a top-flight performer in the online language performance shootout (shootout.alioth.debian.org), comparable with Java Server-6, and approaching native C in performance overall. This is a tribute to the incredible amount of profound optimization built into the compiler, with techniques like cross-module code migration, unboxed data types, and automated removal of intermediate data structures, all done through correctness-preserving transformations that exploit the algebraic simplicity of Haskell terms, even in the presence of monadic effects.

The impact GHC has had on programming language research would be sufficient to merit an award by itself, but GHC is having a corresponding influence in industry. By showing the feasibility of purely functional, statically-typed programming in the large, GHC Haskell has also had clear influence on many of the newest generation of languages, such as C#, F#, Java Generics, LINQ, Perl 6, Python, and Visual Basic 9.0. As Soma Somasegar, Microsoft Developer Division Chief, said in 2007, “One of the important themes in programming languages over recent years has been a move to embrace ideas from functional programming, [which] are helping us address some of the biggest challenges facing the industry today, from the impedance mismatch between data and objects to the challenges of the multi-core and parallel computing space.”

GHC now supports a burgeoning professional Haskell world. The O’Reilly book Real World Haskell, targeted to professional programmers and oriented to GHC, was published in 2008. It went on to win the Jolt Award for best technical book of the year. In 2009 there were 3500+ Haskell package updates, with more than 100,000 package downloads in November alone. GHC is now used across the financial sector in institutions like Credit Suisse and Standard Chartered Bank, and for high assurance software in companies like Amgen, Eaton, and Galois. Some of these companies came together in 2009 to create the Industrial Haskell Group, whose purpose is to ensure the health and longevity of GHC.

499 words. Whew! There is so much that could be said, but let’s hope this is enough. I think the case is very strong, and both Simon’s deserve honor and accolade for their work. Thank you both so much!

Posted in Functional Programming, Haskell, Open Source | Comments (4)

Tech Talk: John Launchbury presents Conal Elliott’s “Beautiful Differentiation”

December 9th, 2009 by Lee Pike

The December 15th Galois Tech Talk will be delivered by John Launchbury. He will present Conal Elliott’s 2009 ICFP paper entitled Beautiful Differentiation for those of us who were not able to attend this wonderful talk in-person.

Date: Tuesday, 10:30am, 15 Dec 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: Automatic differentiation (AD) is a precise, efficient, and convenient method for computing derivatives of functions. Its forward-mode implementation can be quite simple even when extended to compute all of the higher-order derivatives as well. The higher-dimensional case has also been tackled, though with extra complexity. This paper develops an implementation of higher-dimensional, higher-order, forward-mode AD in the extremely general and elegant setting of calculus on manifolds and derives that implementation from a simple and precise specification.

In order to motivate and discover the implementation, the paper poses the question, “What does AD mean, independently of implementation?‚” An answer arises in the form of naturality of sampling a function and its derivative. Automatic differentiation flows out of this naturality condition, together with the chain rule. Graduating from first-order to higher-order AD corresponds to sampling all derivatives instead of just one. Next, the setting is expanded to arbitrary vector spaces, in which derivative values are linear maps. The specification of AD adapts to this elegant and very general setting, which even simplifies the development.

Bio: John Launchbury is the founder and Chief Scientist of Galois, Inc.

Posted in Functional Programming, Haskell, Misc, Tech Talks | Comments (2)

Tech Talk: Testing First-Order-Logic Axioms in AutoCert

October 28th, 2009 by Levent Erkok

The November 3rd Galois Tech Talk will be delivered by Ki Yung Ahn, titled “Testing First-Order-Logic Axioms in AutoCert.”

Date: Tuesday, November 3rd, 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: AutoCert is a formal verification tool for machine generated code in safety critical domains, such as aerospace control code generated from MathWorks Real-Time Workshop. AutoCert uses Automated Theorem Proving (ATP) systems based on First-Order-Logic (FOL) to formally verify safety and functional correctness properties of the code. These ATP systems try to build proofs based on user provided domain-specific axioms, which can be arbitrary First-Order-Formulas (FOFs). That is, these axioms are the crucial trusted base in AutoCert. However, formulating axioms correctly (i.e. precisely as the user had really intended) is non-trivial in practice, and speculating validity of the axioms from the ATP systems is very hard since theorem provers do not give examples or counter-examples in general.

We adopt the idea of model-based testing to aid axiom authors to discover errors in axiomatization. To test the validity of axioms, users can define a computational model of the axiomatized logic by giving interpretations to each of the function symbols and constants as computable functions and data constants in a simple declarative programming language. Then, users can test axioms against the computational model with widely used software testing frameworks. The advantage of this approach is that the users have a concrete intuitive model with which to test validity of the axioms, and can observe counterexamples when the model does not satisfy the axioms. We have implemented a proof of concept tool using Template Haskell, QuickCheck, and Yices.

(This is a joint work with Ewen Denney at SGT/ NASA Ames Research Center, going to be presented in the poster session at Asian Symposium on Programming Languages and Systems this December.)

Bio: Ki Yung Ahn is a Ph.D student at Portland State University working with Tim Sheard and other members of the TRELLYS project, designing and implementing a dependently typed programming language that is general purpose programming friendly. He received a BS in Computer Science from KAIST in 2002, worked as online storage service server programmer at Gretech before joining graduate program at Portland State University in 2005. He has been working on Shared Subtypes, Korean translation of “Programming in Haskell” by Graham Hutton, and enjoying other small funs of Haskell hacking.

Posted in Community, Formal Methods, Functional Programming, Tech Talks, Technology | Comments (0)

Tech Talk: How to choose between a screwdriver and a drill

October 20th, 2009 by Levent Erkok

The October 27th Galois Tech Talk will be delivered by Tanya Crenshaw, titled “How to choose between a screwdriver and a drill.”

Date: Tuesday, October 27th, 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: Suppose you have two different algorithms to compute the same result. One is clearly safe. It is simple enough to verify. The other has more desirable features, but it is too complicated to verify. You want a system that can choose between these two algorithms while meeting its quality of service goals. This is the intuition behind Lui Sha’s Simplex Architecture. The intuition is simple, but its verification is not. Implementations of the Simplex Architecture are reactive systems whose properties are not always easy to express. In this talk, I’ll describe the history of Simplex, the challenges of verifying its safety properties, and a variety of approaches to modeling it, from an architecture description language to an executable specification language.

Bio: Tanya L. Crenshaw is an assistant professor of computer science at the University of Portland. She teaches courses in both Computer Science and Electrical Engineering and conducts research into security for embedded systems. Before University of Portland, she worked for Wind River and Sharp Microelectronics and studied at the University of Illinois at Urbana-Champaign where she completed her Ph.D. (Her personal web-page is at: http://kaju.dreamhosters.com/.)

Posted in Formal Methods, Functional Programming, Tech Talks, Technology | Comments (0)

Tech Talk: Writing Linux Kernel Modules with Haskell

October 13th, 2009 by Levent Erkok

The October 20th Galois Tech Talk will be delivered by Thomas DuBuisson, titled “Writing Linux Kernel Modules with Haskell.”

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

Slides for this talk are now available.

Abstract: Current operating systems are developed and extended primarily with imperative languages that lack in expressiveness and safety. Pure and functional languages fill these gaps nicely but existing tools are not ideal fits and the language abstracts away important environmental information.

This talk will focus on modifications of the Glasgow Haskell Compiler to generate suitable code and nuances of binding to the Linux API. Short-comings of the language and tools will be identified along with known workarounds and potential engineering efforts.

Bio: Thomas DuBuisson is a PhD student in Computer Science at Portland State University, working with advisor Andrew Tolmach. Current research efforts revolve around the use of functional languages for systems programming and improving runtime system security.

Posted in Functional Programming, Tech Talks, Technology | Comments (5)

Domain Specific Languages for Domain Specific Problems

October 13th, 2009 by donstewart

We have a new position paper on the use of EDSLs and Haskell for tackling the “programmability gap” of emerging high performance computing architectures — such as GPGPUs. It will be presented tomorrow at LACSS in Santa Fe. (Download) :: PDF

Slides for the talk, including a 10 minute guide to EDSLs in Haskell, and a 10 minute guide to multicore programming in Haskell, can be found here :: PDF.

Domain Specific Languages for Domain Specific Problems
Don Stewart, Galois.
Workshop on Non-Traditional Programming Models for High-Performance Computing, LACSS 2009.

As the complexity of large-scale computing architecture increases, the effort needed to program these machines efficiently has grown dramatically. The challenge is how to bridge this “programmability gap”, making the hardware more accessible to domain experts. We argue for an approach based on
executable embedded domain specific languages (EDSLs)—small languages with focused expressive power hosted directly in existing high-level programming languages such as Haskell. We provide examples of EDSLs in use in industry today, and describe the advantages EDSLs have over general purpose languages in productivity, performance, correctness and cost.

Thanks to Magnus Carlsson, Dylan McNamee, Wouter Swiestra, Derek Elkins and Alex Mason for feedback on drafts.

Posted in Functional Programming, Haskell | Comments (2)