When writing software that uses open source libraries, the license of a dependency is a real concern. It becomes necessary to watch for license compatibility, as well as ensure that the terms of the license are satisfied when doing a source distribution.As a first attempt at license compatibility checking, we have added some extra checks in the configure step for Cabal, so that warnings will be generated if any direct dependencies have licenses that conflict with that of the configured package [1]. However, there are some limitations to this approach. First, this doesn’t rule out the possibility that a dependency of a package that is deemed compatible will conflict with the license of your executable. Second, it doesn’t allow for a BSD3 library to depend on a GPL library, where the conflict is only produced when an executable is produced from the combination.Some licenses place requirements on how a source or binary distribution can happen. For example, the BSD3 license requires you to include its copyright notice in any distribution you make.In order to speed up this process, we decided to try to extract this information from the GHC package database. According to the GHC manual, the license file should be tracked by the package database, though upon closer inspection, that field doesn’t seem to be tracked. In order to address this shortcoming, we developed a small patch to add this functionality in GHC and Cabal [2]. Using this patched version of GHC and Cabal, we’ve developed a small tool to walk the dependencies of a cabal package, and collect the license files that they have registered in the package database.Both of these patches are available for you to try out, attached to the tickets below, though they have been accepted and are expected to make it into the next release of Cabal.[1] http://hackage.haskell.org/trac/hackage/ticket/481[2] http://hackage.haskell.org/trac/hackage/ticket/710

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:

abcBridge: Functional interfaces for AIGs and SAT solving (slides, video)

presenter:

Edward Z. Yang

time:

10:30am, Tuesday, 24 August 2010

location:

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:

SAT solvers are perhaps the most under-utilized high-tech tools that the modern software engineer has at their fingertips. An industrial strength SAT solver can solve most human generated NP-complete problems in time for lunch, and there are many, many practical problem domains which involve NP-complete problems. However, a major roadblock to using a SAT solver in your every day routine is translating your problem into SAT, and then running it on a highly optimized SAT solver, which is probably implemented in C or C++ and not your usual favorite programming language.This talk is about the use, design and implementation of abcBridge, a set of Haskell bindings for ABC, a system for sequential synthesis and verification produced by the Berkeley Logic Synthesis and Verification Group. ABC looks at SAT solving from the following perspective: given two circuits of logic gates (ANDs and NOTs), are they equivalent? ABC is imperative C code: abcBridge provides a pure and type-safe interface for building and manipulating and-inverter graphs. We hope to release abcBridge soon as open source.

bio:

Edward Z. Yang is an undergraduate studying computer science at MIT. He has been interning at Galois over the summer and enjoying every second of it. His interests include blogging, functional programming and practical applications of computer science research. You can read his blog at http://blog.ezyang.com/

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:

Towards a High-Assurance Runtime System: Certified Garbage Collection

presenter:

Andrew Tolmach

time:

10:30am, Tuesday, 29 June 2010.

location:

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:

It seems obvious that the reliability of critical software can be improved by using high-level, memory-safe languages (Haskell, ML, Java, C#, etc.). But most existing implementations of these languages rely on large, complex run-time systems coded in C. Using such an RTS leads to a large “credibility gap” at the heart of the assurance argument for the overall system. To fill this gap, we are working to build a new high-assurance run-time system (HARTS), using an approach grounded in machine-assisted verification, with an initial focus on providing certifiably correct garbage collection.This talk will describe a machine-certified framework for correct compilation and execution of programs in garbage-collected languages. Our framework extends Leroy’s Coq-certified Compcert compiler and Cminor intermediate language. We add a new intermediate language, GCminor, that supports GC’ed languages and has a proven semantics-preserving translation to assembly code. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verification, including full semantics preservation, type preservation, or informal trust. As an example application of our framework, we describe a compiler for Haskell that translates the GHC’s Core intermediate language to GCminor. (This is joint work with Andrew McCreight and Tim Chevalier.)

bio:

Andrew Tolmach has been a faculty member at Portland State University since receiving his Ph.D.in Computer Science from Princeton in 1992. His current research interests, pursued under the aegis of the PSU High Assurance Systems Programming (HASP) project, focus on high-assurance systems software development, in particular using formal verification. His past publications, mostly about functional languages, include work on operating systems in Haskell, garbage collection, compilation, debugger implementation, integration with logic languages, and lazy functional algorithms.

Orc is a concurrent scripting language, now available as an embedded DSL in Haskell. I like to think of Orc as the combination of three things: many-valued concurrency, external actions (effects), and managed resources, all packaged in a high-level set of abstractions that feel more like scripting rather than programming. It provides a very flexible way to manage multiple concurrent actions, like querying remote web sites, along with timeouts and default actions.Source code is available on Hackage; the easiest way to access it is with cabal (i.e. ‘cabal install orc’).Also available is a draft paper entitled Concurrent Orchestration in Haskell which explains how to use Orc, as well as describing the implementation in detail.Feedback welcome. Enjoy!

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

titile:

Introducing Well-Founded Recursion (slides)

presenter:

Eric Mertens

time:

10:30am, Tuesday, 15 June 2010.

location:

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:

Implementing recursive functions can be tricky when you want to be certain that they eventually terminate. This talk introduces the concept of well-founded recursion as a tool for implementing recursive functions. It implements these concepts in the Agda programming language and demonstrates the technique by implementing a simple version of Quicksort.

bio:

Eric is a member of the technical staff at Galois, Inc., where he holds roles in software design and development for projects focusing on secure collaboration and secure network protocols. He specializes in Haskell programming and in leveraging Haskell’s unique type-system to improve various network and web-focused interfaces.

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

IMPORTANT: Please note that this talk is Monday.

title:

The L4.verified Project

presenter:

Dr. Gerwin Klein

time:

10:30 am, 24 May 2010, Monday

location

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:

Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security.

bio:

Dr Gerwin Klein is a Principal Researcher at NICTA and Conjoint Associate Professor at the University of New South Wales, Australia. He is working in the area of formal software verification, interactive theorem proving, and operating systems. He is the project leader of L4.verified. He received his PhD in 2003 from Technische Universitaet Munich on the topic of Java Bytecode Verification and has been working in the area of machine-checked formal proof in various projects since 1998.

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title

Developing Good Habits for Bare-Metal Programming (slides, video)

presenter

Mark Jones

High Assurance Systems Programming Project (HASP)

Portland State University

time

10:30am, Tuesday, 18 May 2010

location

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract

Developers of systems software must often deal with low-level and performance-critical details that are hard to address in high-level programming languages. As a result, much of the systems software that is produced today is written in languages like C and assembly code, without the benefit of more expressive type systems or other features from modern functional programming languages that could help to increase programmer productivity or software quality. In this talk, we present an update on the status of Habit, a dialect of Haskell that we are designing, as part of the HASP project at PSU, to meet the needs of high assurance systems programming. Among other features, Habit provides: mechanisms for fine control over representation of bit-level and memory-based data structures; strong support for both functional and imperative programming; and a flexible type system that allows precise characterization of size and bound information via type level naturals, as well as termination properties resulting from the use of unpointed types.

bio

(from http://web.cecs.pdx.edu/~mpj/)Mark Jones is a Professor in the Department of Computer Science in the Maseeh College of Engineering & Computer Science at Portland State University in Portland, Oregon, USA. His interests include all aspects of programming language design, implementation, and application. He is particularly interested in the use of advanced programming language technologies for systems programming, and in the development and application of expressive type and module systems that support the construction and certification of secure and reliable software systems.

Please note the non-standard time and day for this talk.Galois is pleased to host the following tech talk.  These talks are open to the interested public.  Please join us!Talks will be held atGalois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

Building Refactoring Tools for Functional Languages

Details:

• Presenter: Prof. Simon Thompson
• Date: Thursday, April 1, 2010
• Time: 10:30am

Abstract: Refactoring is the process of changing the design of a program without changing what it does. Typical refactorings, such as function extraction and generalisation, are intended to make a program more amenable to extension, more comprehensible and so on. Refactorings differ from other sorts of program transformation in being applied to source code (rather than within the bowels of a compiler), and in having an effect across a code base. Because of this, there is a need to give (semi-)automated support to the process. This talk will reflect on our experience of building tools to refactor functional programs written in Haskell and Erlang (Wrangler). In doing this we will address system design, the pragmatics of system take-up, as well as contrasting the style of refactoring and tooling for Haskell and Erlang.Bio: Simon Thompson is a Professor of Logic and Computation at the University of Kent.

LATE NOTICE: The Simon Thompson talk has been moved to Thurs. April 1, at 10:30am.Please note the non-standard times for these talks.Galois is pleased to host two tech talks during the week of March 22, 2010.  The two talks are short (20-30 minutes each) talks back-to-back at 10:30am on March 24th. Details are below.Talks will be held atGalois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)These talks are open to the interested public.  Please join us!

Visualization and Diversity Information

Details:

• Presenter: Prof. Ron Metoyer
• Date: Wednesday, March 24, 2010
• Time: 10:30am

Abstract: The term “diversity’’ is used in many ways in many domains.  People are concerned about the diversity of their work force, stock portfolios, student body, and forest insects, just to name a few.  In this talk, I will discuss a work-in-progress visualization technique specifically designed to communicate diversity information.  I will present the design concerns, resulting visualizations, and a study design for evaluating the method.  I will conclude with a discussion of a case-study application to moth species data.Bio: Ronald Metoyer is an Associate Professor in the School of Electrical Engineering and Computer Science at Oregon State University.  He earned a Ph.D. from the Georgia Institute of Technology where he worked in the Graphics, Visualization and Usability Center with a focus on modeling and visualizing the motion of pedestrians in urban and architectural scenes.  Dr. Metoyer currently co-directs the NVIDIA Graphics and Imaging Technologies Lab (GAIT) with his colleagues at OSU. His past research efforts have involved the investigation of techniques for manipulating motion capture data and for facilitating the creation of 3D content by end users with the goal of empowering domain experts to create compelling and interactive content for their domain specific needs.  In 2002, he received an NSF CAREER Award for his work in “Understanding the Complexities of Animated Content”.  Dr. Metoyer’s most recent research interests fall under the domain of information visualization.

TITLE: Scientific Data Visualization in a GPU World

Details:

• Presenter: Prof. Mike Bailey
• Date: Wednesday, March 24, 2010
• Time: 11:00am

Abstract: One of the fun aspects of scientific data visualization is that there are no rules — anything that adds insight to the data display is fair game.  Add that to the fun of custom-programming the GPU, and you’ve really got something!This talk will discuss some of the uses of custom GPU programming to create better and more interactive visualization displays.  We will look at techniques in the realm of scalar visualization, vector visualization, volume visualization, and terrain mapping.Bio: Mike Bailey is a Professor in Computer Science at Oregon State University. He specializes in scientific visualization, 3D interactive computer graphics, GPU programming, stereographics, and computer aided geometric design.

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)

• View slides online
• Download PDF

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.