Tech talk: Combining Denotational and Operational Semantics for Scalable Proof Development

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

title:Combining Denotational and Operational Semantics for Scalable Proof Development

speakers:Adam Foltzer

time:Tuesday, 19 July 2011, 10:30am

location:

Galois Inc.

421 SW 6th Ave. Suite 300,

Portland, OR, USA

(3rd floor of the Commonwealth building)

abstract:Interpreters offer a convenient and intuitive way for programmers to reason about language behavior through denotational semantics. However in a setting like Coq, where all recursive functions must provably terminate, it is impossible to write interpreters for non-terminating languages. The standard alternative is to inductively define operational semantics, but this can yield proofs that are difficult to automate, particularly in the presence of changing language features.

This talk presents a combined approach, where an interpreter is used in combination with operational semantics to prove type preservation of a small functional language. To demonstrate the scalability of the Coq development, let expressions and a pair types will be added and preservation will be proved again with only one extra line of proof script.

This technique and development are adapted from Greg Morrisett's lectures at the 2011 Oregon Programming Languages Summer School, and are available at his web site.

bio: Adam Foltzer is an Intern at Galois, Inc. and a Master's student at Indiana University studying programming languages.

Merging SMT solvers and programming languages

Galois is in the business of building trustworthy software. Such software will have well-defined behavior, and that behavior is assured in some way, whether via model checking, testing, or formal verification. SMT solvers -- extensions to SAT solvers with support for variables of non-boolean type -- offer powerful automation for solving a variety of assurance problems in software. We use them, for example, in Cryptol, to prove the equivalence (or otherwise) of algorithm implementations.

For a while now, Galois has been interested in connecting automated solvers to our programming language of choice, Haskell, to make it possible to prove automatically some properties of our functions (rather than just testing, e.g. with QuickCheck). We've pushed two efforts out this week, as previews of what we're thinking in this space:

• SBV; and


• yices-painless.

Both are embedded DSLs for representing propositions to an SMT solver via Haskell functions and values. They take different approaches (a compiler from Haskell to the SMT-LIB format, versus an interpreter for the Yices SMT solver). SBV is the more mature package, while yices-painless emphasizes a type-preserving translation from a minimal core language. SBV was built by Levent Erkok, yices-painless by Don Stewart. Documentation for the design of yices-painless is available, as is documentation on SBV.

Both are ready for experimentation and feedback, and we welcome your comments.

Copilot and the Arduino

Copilot is an embedded domain-specific language designed by Galois, that allows you to generate assured, embedded C code from programs written essentially as Haskell lists (using Atom as a backend for the C code generation).

 Lee Pike has written a tutorial on how to use Copilot to program an Arduino controller to play “Jingle Bells”. Read the full tutorial on Lee's Critical Systems Blog...

Building a business with Haskell: Case Studies: Cryptol, HaLVM and Copilot

During BelHac, the Ghent Haskell Hackathon in November, we took an afternoon session for a "Functional Programming in Industry" impromptu workshop. The following are slides I presented on Galois' experience building a business using our functional programming expertise, in particular, Haskell.

The talk describes three case studies where "functional thinking" helped shape the solution to the client's problem, whether via types, semantics, abstractions or otherwise. The examples are taken from the Cryptol, Embedded Systems and Secure Networking research programs at Galois. A PDF of the slides are also available.

Building a business with Haskell: Case Studies: Cryptol, HaLVM and Copilot

More about functional programming at Galois...

Galois releases the Haskell Lightweight Virtual Machine (HaLVM)

Galois, Inc. is pleased to announce the immediate release of the Haskell Lightweight Virtual Machine (or HaLVM), version 1.0. The HaLVM is a port of the GHC runtime system to the Xen hypervisor, allowing programmers to create Haskell programs that run directly on Xen’s “bare metal.” Internally, Galois has used this system in several projects with much success, and we hope y’all will have an equally great time with it.

What might you do with a HaLVM? Pretty much anything you want. :) Explore designs for operating system decomposition, examine new notions of mobile computation with the HaLVM and Xen migration, or find interesting network services and lock them inside small, cheap, single-purpose VMs.

The HaLVM is the result of many years of effort, by many people inside Galois.  Although it is not yet totally bug-free, we have decided that broad adoption wins over perfection and thus we are releasing it for general review. As such, there will be some rough edges, and we urge you to read the documentation to understand the platforms we test on.

We are releasing the HaLVM under a non-restrictive BSD3 license. You can find it here:

http://halvm.org

We welcome user feedback, feature requests, bug notices, patches, and feature additions; see the page above for guidelines on getting involved.

Finally, we’d like to give many things to the GHC and Xen communities, without which this work would not be possible.

If you have any questions or concerns, please don’t hesitate to contact the HaLVM’s maintainers at halvm-devel@community.galois.com.

Have a lovely day!