Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
title:
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study
presenter:
Joe Hendrix
time:
10:30am, Tuesday, 22 June 2010.
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
Many inductive theorem provers use induction schemes derived from the recursive calls in functions definitions. This widely-used strategy is called coverset induction in the context of algebraic specifications. One challenge in applying coverset induction is that it typically requires using a total recursive function, while many operations on data structures are only meaningful on some well-formed subset of their possible inputs.
In this talk, I’ll discuss a generalization of coverset induction to handle partial constructors and operations. The generalization is implemented in the Maude ITP, and used in an extensive case study involving powerlists — a data structure introduced by J. Misra to elegantly formalize parallel algorithms based on divide and conquer strategy. Powerlists are constructed by partial operations, and it has been a challenge to naturally reason about powerlists using a formal logic that only supports total operations. We show how theorems about powerlists can be elegantly proven using the generalized coverset induction scheme implemented in the Maude ITP.
bio:
Joe is a member of the technical staff at Galois, Inc. He is interested in developing tools for making software development easier and safer. He started out developing software for civil engineers to analyze the safety of bridge foundations. He worked on automated decision procedures during his PhD at the University of Illinois. Immediately prior to joining Galois, he developed software within Microsoft’s Trustworthy Computing Initiative.
We are pleased to announce the availability of a new Galois tech talk video: “Databases are Categories”, presented by David Spivak. More details about the talk are available on the announcement page.
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!
For a number of years, Galois Inc. has been organizing technical seminars presented by visiting researchers, Galois engineers, and members of the vibrant Portland technical community. The seminars span a wide variety of topics, ranging from functional programming, formal methods, and compiler and language design, to cryptography, and operating system construction. The talks are free and open to the interested public. Announcements of upcoming talks are posted to this blog about a week in advance.Over the last few months we have received a number of requests to share videos of the talks with the wider community. As a result, we are very pleased to announce the Galois tech talk channel on Vimeo. Recent Galois talks should become available over the next few weeks, followed by future presentations.Enjoy!Galois tech talk channel: http://vimeo.com/channels/galois
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!
title:
Large-Scale Static Analysis at Mozilla (slides, video)
presenter:
Taras Glek
time:
10:30 am, 8 June 2010, Tuesday
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
A competitive browser market requires fast-paced improvements to the codebase. Such improvements may require significant refactoring of large parts of the codebase. Mozilla Firefox is one of the largest open source C++ projects. Unfortunately C++ is a complex language: method overloading, virtual functions, template instantiation, pointer arithmetic, etc reduce developer productivity. Mozilla developed C++ static analysis and refactoring tools to increase developer leverage in C++. Static analysis is done via Dehydra/Treehydra GCC plugins and refactoring is accomplished by extending the Elsa C++ parser. This talk will discuss why Mozilla needs static analysis, why there are so few tools for C++, and specific projects that we’ve embarked on.
bio:
Taras Glek is a software engineer at Mozilla Corporation. He works on static analysis and startup performance. Taras blogs about it at http://blog.mozilla.com/tglek/.
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 Thursday.
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
Category theory is a powerful language for organizing layers of abstraction in all areas of mathematics. Databases are powerful tools for organizing information of all sorts. Whereas categories are often considered hopelessly abstract, databases are often considered horrifically mundane. Thus it is either strange or fitting that, mathematically speaking, categories and databases are the same concept. In this talk I’ll show how to turn any database into a category and any category into a database. I’ll also discuss functors and how they may be useful for issues of data migration and merging.
bio:
David Spivak graduated with a PhD in mathematics from UC Berkeley in 2007; his thesis used higher category theory to fix an old problem in geometry. From 2007 to the present, he have been a postdoc at the University of Oregon in the Math Department. During this time, his focus has moved toward the idea of using category theory to understand information and communication. This summer, he will become a mathematics postdoc at MIT for three years, focusing on information and communication from a category-theoretic perspective.
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.
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!The talk will be held atGalois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
Typing DirectoriesDetails:
Presenter: Kathleen Fisher, AT&T Labs
Date: Monday May 03, 2010
Time: 3:30pm (NOTE THE CHANGED DATE AND TIME!)
Abstract: PADS describes the contents of individual ad hoc data files, but has no provisions for describing collections of files, i.e., directories. In this talk, I explore examples where having a declarative description of directories as well as files would be useful, including websites, source code trees, source code control systems, operating systems, and scientific data sets. As part of this exploration, I identify essential features of a directory description language and useful tools that might be produced from such a description. I end with a series of questions about how such a language might most easily be implemented in the context of Haskell.This is joint work with David Walker and Kenny Zhu.Bio: (from http://www.research.att.com/people/Fisher_Kathleen_S) Kathleen Fisher is a Principal Member of the Technical Staff at AT&T Labs Research and a Consulting Faculty Member in the Computer Science Department at Stanford University. Kathleen’s research focuses on advancing the theory and practice of programming languages and on applying ideas from the programming language community to the problem of ad hoc data management. The main thrust of her work has been in domain-specific languages to facilitate programming with massive amounts of ad hoc data, including the Hancock system for efficiently building signatures from massive transaction streams and the PADS system for managing ad hoc data.Kathleen is an ACM Distinguished Scientist. She has served as program chair for FOOL, CUFP, and ICFP. She is past Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN), Co-Chair of CRA’s Committee on the Status of Women (CRA-W), and an editor of the Journal of Functional Programming. She is currently serving on the CRA Board.
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.