Wednesday
Apr032013

Tech Talk: Introducing HERMIT, a Plugin for Transforming GHC Core Language Programs

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: Introducing HERMIT: A Plugin for Transforming GHC Core Language Programs

speaker: Andrew Farmer

time: Tuesday, 09 April 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks, leaving the programmer to do them by hand. This talk introduces HERMIT, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Haskell Compiler's optimization pipeline. With HERMIT, users can experiment with optimizations and equational reasoning, while the tedious heavy lifting of performing the actual transformations is done for them. The talk will explore design choices in HERMIT, demonstrate its use on examples, and seek input for further development and case studies.

bio:

Andrew Farmer is a Ph.D. student at the University of Kansas, working with Andy Gill. He received his B.S. in Computer Science from the University of Kansas in 2005 and went off to industry to write domain specific languages for web application development. Returning to KU in the fall of 2009, Andrew's interests include programming language design in general and specifically the compilation and optimization of functional languages. He has done work on testing and debugging tools for the Kansas Lava project. He is currently working on the HERMIT project, where he is interested in leveraging HERMIT's capabilities to write domain-and-program-specific optimizers.

Thursday
Mar072013

Tech Talk: Inferring Phylogenies Using Evolutionary Algorithms

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: Inferring Phylogenies Using Evolutionary Algorithms

speaker: Erlend Hamberg

time: Tuesday, 12 March 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

An important problem in genetics is phylogenetic inference: Coming up with good hypotheses for the evolutionary relationship between species – usually represented as a “family tree”. As the amount of molecular data (e.g. DNA sequences) quickly grows, efficient algorithms become increasingly important to analyze this data. A maximum-likelihood approach with models for nucleotide evolution allows us to use all the sequence data, but is a computationally expensive approach. The number of possible trees also grows rapidly as we include more species. It is therefore necessary to use heuristic search methods to find good hypotheses for the “true” tree. Evolutionary algorithms (EA) is a class of such search/optimization algorithms that has been shown to perform well in other areas where the search space is large and irregular. I will explain my approach and my findings from using an evolutionary algorithm for inferring phylogenies from molecular data.

bio:

Erlend Hamberg obtained his M.Sc. in Computer Science from the Norwegian University of Science and Technology (NTNU) in 2011. For his Master's thesis research he worked on the problem of inferring phylogenies (i.e. the evolutionary relationship between species) from molecular data. He was previously at ARM where he worked on the drivers for Mali series of GPUs.

Thursday
Feb282013

Tech Talk: Parametricity, Quotient types, and Theorem transfer

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: Parametricity, Quotient types, and Theorem transfer

speaker: Brian Huffman

time: Tuesday, 05 March 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

A polymorphic function may be instantiated at many different types; if the function is parametrically polymorphic, then all of its instances must behave uniformly. Reynolds' parametricity theorem expresses this precisely, in terms of binary relations derived from types. One application of the parametricity theorem is to derive Wadler-style "free theorems" about a polymorphic function from its type; e.g. rev :: [a] -> [a] must satisfy map f (rev xs) = rev (map f xs).

In this talk, I will show how to apply many of the ideas behind parametricity and free theorems in a new setting: formal reasoning about quotient types. Using types-as-binary-relations, we can automatically prove that corresponding propositions about quotient types and their representation types are logically equivalent. This design is implemented as the Transfer package in the Isabelle theorem prover, where it is used to automate many proofs about quotient types.

bio:

Brian Huffman is a recent PhD graduate from the Department of Computer Science at Portland State University, now at Galois after completing 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.

Wednesday
Feb062013

Tech Talk: Automatic Function Annotations for Hoare Logic

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: Automatic Function Annotations for Hoare Logic

speaker: Daniel Matichuk

time: Tuesday, 12 February 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Formal verification can provide a high degree of assurance for critical software, but can come at the cost of large artefacts that must be maintained alongside it. When using an interactive theorem prover, these artefacts take the form of large, complex proofs where the ability to reuse and maintain them becomes paramount. I will present my work on a function annotation logic, which is an extension to Hoare logic that allows reasoning on intermediate program states to be easily reused. Program functions are annotated with properties as a side-condition of existing proofs. These annotations can reduce the proof burden substantially when subsequent program properties need to be shown. Implemented in Isabelle, it is shown to be practically useful by greatly simplifying cases where existing proofs contained largely duplicated reasoning.

bio:

Daniel Matichuk obtained his B.Sc. in Honors Computer Science from the University of Alberta, Canada in 2011 and has since been working at NICTA in Sydney as a Research Engineer. He will soon be starting his PhD at NICTA and the University of New South Wales. His recent work was aiding in the noninterference proof for the seL4 microkernel and he is interested in maintenance and refactoring in large formal proofs.

Thursday
Nov292012

Tech Talk: Computers and privacy, ACLU of Oregon discusses their 2013 agenda

(There is no need to pre-register for the talk.)

title: Computers and privacy, ACLU of Oregon discusses their 2013 agenda

speaker: Becky Straus

time: Tuesday, 4 December 2012, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Efforts at the federal level to pass laws like the Stop Online Piracy Act (SOPA) and the Cyber Intelligence Sharing and Protection Act (CISPA) have attracted widespread attention and criticism, and rightly so. But Washington, D.C. is far from the only place that officials are making decisions that impact the privacy and free speech rights. State and local officials are jumping into the fray as well, passing laws or creating policies that have immediate impact without the spotlight that accompanies federal action. The fact is that privacy laws have failed to keep up with emerging technologies. This presentation will survey several areas where state and local officials in Oregon have recently been active, including reviewing policies on automated license plate recognition, surveillance cameras, and use of domestic drones. We will discuss how the ACLU of Oregon has been involved and what is on our agenda for the upcoming 2013 state legislative session.

bio:

Becky Straus is the legislative director for the American Civil Liberties Union of Oregon. She joined the staff in 2011 and directs ACLU’s advocacy and lobbying efforts before the Oregon Legislature and coordinates ACLU testimony before public bodies on the full range of civil liberties and civil rights issues in Oregon. She is also ACLU’s primary lobbyist on City of Portland matters.

Page 1 ... 5 6 7 8 9 ... 49 Next 5 Entries »