Tech Talk: Making GHC work for you

abstract: GHC is a state-of-the-art optimizing compiler that is constantly being improved. But despite all of the hard work by the developers, you occasionally find yourself in need of a feature that GHC does not (yet) support. Luckily for us, GHC does have multiple extension points built into the standard compilation pipeline, in addition to […]

Read More

(Ab)using Compiler Plugins to Improve Embedded DSLs

by Eric Seidel, Galois intern Embedded DSLs are a bit of a double-edged sword. They have a low start-up cost because you can defer a lot of work to the host language, but producing good error messages can be challenging. People often talk about the quality of type errors produced by the host language, but […]

Read More

Block Ciphers, Homomorphically

by Brent Carmer and David W. Archer, PhD Our team at Galois, Inc. is interested in making secure computation practical. Much of our secure computation work has focused on linear secret sharing (LSS, a form of multi-party computation) and the platform we’ve built on that technology. However, we’ve also done a fair bit of comparison […]

Read More

Tech Talk: Read-copy update (RCU) validation and verification for Linux

abstract: Read-copy update (RCU) is a synchronization mechanism that is sometimes used as an alternative to reader-writer locking (among other things) that was added to the Linux kernel in 2002. A similar mechanism was added to Sequent’s DYNIX/ptx parallel UNIX kernel in 1993, and antecedents go back to at least 1980. Although a fully functional […]

Read More

Innovation Week: Experiments, prototypes and new skills

During the first week of October, Galois held “Innovation Week,” a time for everybody to explore new ideas, recharge our creativity, have fun and share what we’ve learned and done with each other. Throughout the week, Galwegians worked on a diverse set of side projects: running experiments, building prototypes, solving puzzles and acquiring new skills.

Read More

Tech talk by Philip Wadler

abstract: We present four calculi for gradual typing: λB, based on the blame calculus of Wadler and Findler (2009); λC, based on the coercion calculus of Henglein (1994); and λT and λW, based on the three- some calculi with and without blame of Siek and Wadler (2010). We define translations from λB to λC, from […]

Read More

Tech Talk: Functional programming in Swift

Galois is pleased to host the following tech talk. These talks are open to the interested public–please join us! (There is no need to pre-register for the talk.) abstract: At this year’s WWDC, Apple announced Swift, a new programming language for iOS and OS X development. In this talk, I’d like to give a brief […]

Read More

Tech talk: Automatic Device Driver Synthesis

abstract: Automatic device driver synthesis is a radical approach to creating drivers faster and with fewer defects by generating them automatically based on hardware device specifications. I will present the design and implementation of a new driver synthesis toolkit, called Termite-2. Termite-2 is the first tool to combine the power of automation with the flexibility […]

Read More

Tech Talk: Verified Cryptographic Implementations

Abstract EasyCrypt is a computer-assisted framework for proving the security of cryptographic constructions. However, there is a significant gap between security proofs done in the usual provable security style and cryptographic implementations used in practice; as a consequence, real-world cryptography is sometimes considered as “one of the many ongoing disaster areas in security. We have […]

Read More