Wednesday
Sep262012
Galois at ICFP 2012
Galois, Inc.Check out these ICFP presentations by Galois team members:
Tuesday
Sep182012
Fill the Bike Racks Day
The Galois office is home to 18 bike racks, about one for every two employees. Tuesday, September 18 was Fill the Bike Racks Day. We didn't fill all the racks, but we still had 15 employee cycles gracing the office today.
Fill the Bike Racks Day was scheduled in September to complement the annual Bike Commute Challenge.
Tuesday
Sep042012
Tech Talk Video: Comprehensive Analysis of the Android Ecosystem
We are pleased to announce the availability of a new tech talk video: "Comprehensive Analysis of the Android Ecosystem", presented by Iulian Neamtiu. For more details, please visit the talk announcement page.
For more videos, please visit our Vimeo channel.
Friday
Aug242012
Tech Talk: Formal Verification of Monad Transformers
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.)
Please note the unusual time for this talk. It is on Thursday at 11am.
title: Formal Verification of Monad Transformers
speaker: Brian Huffman
time: Thursday, 30 August 2012, 11:00am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type quantification; instead, we rely on a domain-theoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses. We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes.
bio:
Brian Huffman is a recent PhD graduate from the Department of Computer Science at Portland State University, now working as a postdoc at the Technical University of Munich. He has been an avid Haskell programmer since 2001, and has contributed to the development of the Isabelle interactive theorem prover since 2005, with an emphasis on tools for verifying lazy functional programs. Several of Brian's formalizations can be found online at the Archive of Formal Proofs.
Tuesday
Aug212012
Tech Talk: Abstract "Anything": Theory and Proof Reuse via DTP
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.)
title: Abstract "Anything": Theory and Proof Reuse via DTP
speaker: Larry Diehl
time: Tuesday, 28 August 2012, 10:30am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
Many advanced branches of mathematics involve structures that abstract over well known specific instances, e.g. abstract algebraic structures, equivalence relations, various orders, category theoretic structures, etc. In typed functional programming (e.g. with type classes in Haskell), encoding such structures amounts to enforcing the definition of elements and operations for a particular structure instance on one hand, and being able to use said elements and operations in generic definitions on the other hand. With Dependently Typed Programming (DTP) we can go one step further and define propositions/properties for abstract structures, and subsequently require proofs in particular instances.
This talk will tell the story of how examples of particular instances inspire an abstract definition (including its propositional properties), how to then instantiate the original concrete examples in the new abstract definition, and finally create further abstract definitions that depend on previously defined ones. Emphasis will be given on how easily concrete proofs can be used as evidence for abstract propositions, and how proofs about abstract structures parameterized by other abstract structures may reuse their proofs (similar to the more common concept of reusing operations in subsequent abstract definitions). The talk will use Agda as its demonstration language, but proofs will mostly be in the form of equational reasoning that should look familiar to the non-expert.
bio: Larry Diehl is an incoming PhD student of Computer Science at Portland State University. He has most recently worked for Engine Yard building infrastructure for deploying web applications to cloud providers, and previously got his bachelor's degree from the University of Central Florida. Larry has been merrily programming in Agda as a hobby for the last few years, and some of his work can be seen on GitHub under the user larrytheliquid.