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.

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.

Duncan Coutts, from Well-Typed, gave a tech talk on Tuesday, 7th Oct, 10.30am, at Galois, about the technical direction of Cabal, Haskell package infrastructure, and the problems of managing large volumes of Haskell code. (.pdf slides).

This will be an informal talk and discussion on two topics:AbstractA language for build systemsBuild systems are easy to start but hard to get right. We’ll take the view of a language designer and look at where our current tools fall down in terms of safety/correctness and expressiveness.We’ll then consider some very early ideas about what a build system language should look like and what properties it should have. Currently this takes the form of a design for a build DSL embedded in Haskell.Constraint solving problems in package deploymentWe are all familiar, at least peripherally, with package systems. Every Linux distribution has a notion of packages and most have high level tools to automate the installation of packages and all their dependencies. What is not immediately obvious is that the problem of resolving a consistent set of dependencies is hard, indeed it is NP-complete. It is possible to encode 3-SAT or Sudoku as a query on a specially crafted package repository.We will look at this problem in a bit more detail and ask if the right approach might be to apply our knowledge about constraint solving rather than the current ad-hoc solvers that most real systems use. My hope is to provoke a discussion about the problem.

Rishiyur Nikhil, CTO of Bluespec, Inc. will be giving a tech talk on Thursday, October 2nd, at 10.30am, about Bluespec SystemVerilog.Abstract

Over the past few years, several projects in major companies have been adopting BSV (Bluespec SystemVerilog) as their next-generation tool of choice for IP design, modeling (for both architecture exploration and early software development), and verification enviroments.The reason for choosing BSV is its unique combination of:

1. excellent computation model for expressing complex concurrency and communication, based on atomic transactions and atomic transactional inter-module methods
2. very high level of abstraction and parameterization (principally inspired by Haskell)
3. full synthesizability, enabling execution on FPGAs, obtaining better performance (3 to 4 orders of magnitude) and scalability than software simulation at comparable levels of detail.

In this presentation, I will provide a brief technical overview of BSV (points 1-3 above), and describe several customer projects using BSV. I will also briefly contrast BSV with other approaches to High Level Synthesis (particularly those based on C/C++/SystemC).

Johan Tibell, from Google, visited Galois on Monday 15th September, and gave a tech talk about efficient IO in Haskell, based on left-fold enumerators, along with a demo of his high perf. Haskell webserver, Hyena, based on left-fold IO. (.pdf slides).For more on left-fold, resource-managing IO subsystems, see Oleg Kiselyov’s work on the best collection traversal interface, From enumerators to cursors: turning the left fold inside out and Peng Li’s work on massively threaded Haskell web servers based on epoll. This stuff is quite hot, with Oleg coincidentally talking about left folds for web servers next week, at DEFUN.

Abstract

I will describe a programming style for I/O operations that is based on left-fold enumerators. This style of programming is more expressive than imperative style I/O represented by the Unix functions read and write, and safer than lazy I/O using streams. Left-fold enumerators offers both high-performance using block based I/O and safety in terms of error handling and resource usage. I will demonstrate Hyena, a web server prototype written in Haskell, as an example of left-fold enumerator style of programming.This talk is intended as a starting point for further discussions on what would be a good interface for I/O rather than a presentation of finished research.

The talk was held at 1pm, on Monday 15th September, at Galois, in Portland.

This Galois Tech Talk was held on Tuesday September 16th, 10.30am, with John Harrison, Principal Engineer at Intel, talking about theorem proving for formal verification. (You can also check out his Handbook of Practical Logic and Automated Reasoning). (.pdf slides, proof demo)

Abstract

The theorem proving approach to verification involves modelling a system in a rich formalism such as higher-order logic or set theory, then performing a human-driven interactive correctness proof using a proof assistant. In a striking contrast, techniques like model checking, by limiting the user to a less expressive formalism (propositional logic, CTL etc.), can offer completely automated decision methods, making them substantially easier to use and often more productive. With this in mind, why should one be interested in the theorem proving approach? In this tutorial I will explain some of the advantages of theorem proving, showing situations where the generality of theorem proving is beneficial, allowing us to tackle domains that are beyond the scope of automated methods or providing other important advantages. I will talk about the state of the art in theorem proving systems and and give a little demonstration to give an impression of what it’s like to work with such a system.

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.

The next Galois Tech Talk will be Tuesday September 9th, 10.30am, with Lee Pike, talking about how to visually present proofs and formal notation.(.pdf slides):Abstract

To the typical engineer or evaluator, mathematics can be scary, logic can be scarier, and really long specifications can simply be overwhelming. This talk is about the problem of the visual presentation of formal specifications clearly and concisely. We take as our initial inspiration Leslie Lamport’s brief papers, “How to Write a Long Formula” and “How to Write a Proof” in which he proposes methods for writing the long and tedious formulas and proofs that appear in formal specification and verification.I will describe the problem and present one particular solution, as implemented in a simple pretty-printer I’ve written (in Haskell), that uses indentation and labels to more easily visually parse long formulas. Ultimately, I propose a “HOL Normal Form” for presenting specifications, much like BNF is used for presenting language definitions.

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.

This Galois tech talk was held on Tuesday, September 2nd, 10.30am. Sean Lee from UNSW, Sydney, talked about programming GPUs from Haskell. Here’ s the abstract  (.pdf slides):GpuGen: Bringing the Power of GPUs into the Haskell WorldAbstract

For the last decade, the performance of GPUs has out-grown CPUs, and their programmability has also improved to the level where they can be used for general-purpose computations. Nonetheless, GPU programming is still limited only to those who understand the hardware architecture and the parallel processing. This is because the current GPU programming systems are based on the specialized parallel processing model, and require low-level attention in many aspects such as thread launching and synchronization.The need for a programming system which provides a high-level abstraction layer on top of the GPU programming systems without losing the performance gain arises to facilitate the use of GPUs. Instead of writing a programming system from the scratch, the development of a Haskell extension has been chosen as the ideal approach, since the Haskell community has already accumulated a significant amount of research and resources for Nested Data Parallelism, which could be adopted to provide a high-level abstraction on GPU programming and even to broaden the applicability of GPU programming. In addition, the Foreign Function Interface of Haskell is sufficient to be the communication medium to the GPU.GpuGen is what connects these two dots: GPUs and Haskell. It compiles the collective data operations such as scan, fold, map, etc, which incur most computation cost, to the GPU. The design of the system, the structure of the GpuGen compiler, and the current development status are to be discussed in the talk.

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. If you’re planning to attend, dropping a note to dons at galois.com is appreciated, but not required. If you’re interested in giving a talk, we’re always looking for new speakers.

Welcome to the Galois blog!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.To kick things off, we’ll start with slides from the past three tech talks, covering formal verification of microkernels, foreign function interface games for Isabelle, and making Haskell arrays faster.Large Scale Monadic Refinement – Tales from L4.verifiedThomas Sewell, proof engineer from NICTA’s L4.verified project, gave a great tech talk about the process of engineering large scale proofs (in this case, for the sel4 microkernel). (.pdf slides)Abstract

Components of operating systems have emerged as an attractive target for formal analysis, thanks to the key importance of operating system correctness in establishing the security of a range of applications. These systems present a number of unique challenges for analysis, including their low level implementation and their detailed view of the system state. This talk will address none of these, instead focusing on the challenges of reasoning about (relatively) large, non-modular, inherently imperative software artefacts.The talk will describe the formalisation of the seL4 microkernel using a state monad with nondeterminism and exceptions, present a refinement and Hoare calculus, and discuss the impact of this chosen approach on the effectiveness of the overall verificationeffort.

PolyML, C, OCaml: Adventures in Foreign Function InterfacesThe August 19th tech talk was Joel Stanley, describing his adventures getting PolyML and OCaml to talk to each other, so that DPT and Isabelle could be friends. (.pdf slides)Abstract

In-process integration and data exchange between multiple language runtimes is a classic software engineering challenge.  This talk describes our experiences in building an open-source tool for generating an “FFI bridge” between Poly/ML and OCaml, via the common C FFI provided by both language’s runtimes.The first intended use of this tool is to programmatically generate a bridge between Isabelle (on the Poly/ML side) and Intel’s Decision Procedure Toolkit API (on the OCaml side).

Stream Fusion for Haskell ArraysThe July 15th tech talk was Don Stewart, talking about stream fusion on Haskell arrays. (.pdf slides)Abstract

Arrays have traditionally been an awkward data structure for Haskell programmers. Despite the large number of array libraries available, they have remained relatively awkward to use in comparison to the rich suite of purely functional data structures, such as fingertrees or finite maps. Arrays have simply not been first class citizens in the language.In this talk we’ll begin with a survey of the more than a dozen array types available, including some new matrix libraries developed in the past year. I’ll then describe a new efficient, pure, and flexible array library for Haskell with a list like interface, based on work in the Data Parallel Haskell project, that employs stream fusion to dramatically reduce the cost of pure arrays. The implementation will be presented from the ground up, along with a discussion of the entire compilation process of the library, from source to assembly.