Tech Talk: Android G1: Experiences with an open mobile platform

The second Galois Tech Talk, for 2009, was Isaac Potoczny-Jones (aka SyntaxNinja) on developing for the Android G1 phone. You can read the slides..

The Android G1 is a TMobile phone whose operating system, Android is based on Linux and was developed by Google. It's a very open smart-phone platform that rivals the iPhone.While I'm no expert in Android or mobile platform development, I will discuss my experiences in Android development and demonstrate the toolchain used to develop software for the Android. I'll outline the basic features of the platform, with a focus on the factors that make its openness so powerful:* the inter-process communications mechanism whereby applications can advertise the services they offer and other applications can take advantage of those services,* The open-source Java, Eclipse, and Linux-based toolchain,* the OpenIntents project.This will be an informal demonstration and discussion.A group of us in collaboration between the Android Password Safe project and the Openintents project have implemented a cryptography service and a keystore service which other Android applications can use to keep data and passwords safe, in a way that's convenient for the end user.Our system allows a single password, and periodic single sign-on so that all applications can encrypt, decrypt, and store keys using the same master password that the user enters once.

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

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.

Click to read more ...

Galois at POPL

The Principles of Programming Languages conference, POPL 09, and its surrounding workshops is kicking off this week in Savannah, Georgia. Galwegians will be attending most of the conferences: you might be able to find Levent at VMCAI or the Twelf Tutorial, or Iavor at TLDI or POPL, and Jeff Lewis (now at Signali) will be giving a keynote at PADL. Step up and say "hello!".

Click to read more ...

Signali: A Custom IP-Design Company

Signali Corp is the latest technology commercialization spinout from Galois, chartered with commercialization of hardware IP core design technology aimed at the FPGA and ASIC markets.  Engineers at Galois and Signali have used the proprietary technology to deliver to government prime contractors the highest performing FPGA implementations in the world for a set of common cryptographic algorithms.With this technology, Signali is well-placed to make a significant impact on the IP core market with their ability to re-tune their cores to meet the customer’s design constraints, whether speed, or power, or area. The technology is especially well suited for optimizing hardware designs of computationally complex functions such as those common in digital signal processing and cryptographic systems.Galois enlisted the experience of Brian Moore, a seasoned design engineer and lab director from Intel, to lead Signali. Moore brings over 25 years of experience in the semiconductor and energy research industries. Galois co-founder Jeff Lewis, is leading the technology development as Chief Technology Officer. Signali is currently co-located with Galois in the historic Commonwealth Building in downtown Portland, Oregon. The company is engaged with Achronix Semiconductor to develop a portfolio of very high performance IP cores for their next-generation FPGAs. Sample performance and utilization numbers for IP cores running on the Achronix Speedster FPGA can be found on the Signali website.

Click to read more ...

Real World Haskell: Intel Parallel Programming Podcast

Don did an interview with Michael Wrinn and Aaron Tersteeg from Intel’s Multicore Software Development podcast about Haskell, multicore and parallel programming, and the use of functional programming at Galois and in industry in general. Listen to the full interview! (15 minutes).

Click to read more ...

Tech Talk: OpenTheory: Package Management for Higher Order Logic Theories

This Galois Tech Talk, the first for 2009, was our very own Joe Hurd talking about package management for theories. You can read the slides

Interactive theorem has grown beyond toy examples in mathematics and program verification, as demonstrated by recent successes such as the Gonthier's formal proof of the four colour theorem and Leroy's verified compiler from a realistic subset of C into PowerPC assembly code. As the construction of large programs led to the development of software engineering techniques, there is now a need for theory engineering techniques to support these major verification efforts.In this talk I will present the OpenTheory project, which has defined a simple 'article' format to represent theories of higher order logic. Theories in article format can be written by one higher order logic theorem prover, compressed by a standalone tool, stored and read by a different theorem prover. Articles naturally support theory interpretations, which leads to more efficient developments of standard theories, and also provides one approach to handling difficult constructs such as monads without extending the underlying logic. Finally, the grand vision of the OpenTheory article repository is painted, with fully automatic installation and dependency resolution.

• Date: Tuesday, January 13, 2008
• Time: 10:30am - 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

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.

Click to read more ...