Tech Talk: Two Talks! One Week!

LATE NOTICE: The Simon Thompson talk has been moved to Thurs. April 1, at 10:30am.Please note the non-standard times for these talks.Galois is pleased to host two tech talks during the week of March 22, 2010.  The two talks are short (20-30 minutes each) talks back-to-back at 10:30am on March 24th. Details are below.Talks will be held atGalois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)These talks are open to the interested public.  Please join us!


Visualization and Diversity Information

Details:

  • Presenter: Prof. Ron Metoyer
  • Date: Wednesday, March 24, 2010
  • Time: 10:30am

Abstract: The term “diversity’’ is used in many ways in many domains.  People are concerned about the diversity of their work force, stock portfolios, student body, and forest insects, just to name a few.  In this talk, I will discuss a work-in-progress visualization technique specifically designed to communicate diversity information.  I will present the design concerns, resulting visualizations, and a study design for evaluating the method.  I will conclude with a discussion of a case-study application to moth species data.Bio: Ronald Metoyer is an Associate Professor in the School of Electrical Engineering and Computer Science at Oregon State University.  He earned a Ph.D. from the Georgia Institute of Technology where he worked in the Graphics, Visualization and Usability Center with a focus on modeling and visualizing the motion of pedestrians in urban and architectural scenes.  Dr. Metoyer currently co-directs the NVIDIA Graphics and Imaging Technologies Lab (GAIT) with his colleagues at OSU. His past research efforts have involved the investigation of techniques for manipulating motion capture data and for facilitating the creation of 3D content by end users with the goal of empowering domain experts to create compelling and interactive content for their domain specific needs.  In 2002, he received an NSF CAREER Award for his work in “Understanding the Complexities of Animated Content”.  Dr. Metoyer’s most recent research interests fall under the domain of information visualization.


TITLE: Scientific Data Visualization in a GPU World

Details:

  • Presenter: Prof. Mike Bailey
  • Date: Wednesday, March 24, 2010
  • Time: 11:00am

Abstract: One of the fun aspects of scientific data visualization is that there are no rules — anything that adds insight to the data display is fair game.  Add that to the fun of custom-programming the GPU, and you’ve really got something!This talk will discuss some of the uses of custom GPU programming to create better and more interactive visualization displays.  We will look at techniques in the realm of scalar visualization, vector visualization, volume visualization, and terrain mapping.Bio: Mike Bailey is a Professor in Computer Science at Oregon State University. He specializes in scientific visualization, 3D interactive computer graphics, GPU programming, stereographics, and computer aided geometric design.

Read More

Tech Talk: An Introduction to Communicating Haskell Processes

Please note the unusual time-slot for this talk!Details:

  • Title: An Introduction to Communicating Haskell Processes
  • Presenter: Neil Brown
  • Date: Monday, 15 March 2010
  • Time: 10:30am
  • Location: Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

Abstract: Haskell is an excellent language for combining the power of functional programming with imperative constructs. This characteristic led to the development of the Communicating Haskell Processes (CHP) libraries, which support imperative synchronous message-passing in Haskell. The core ‘chp’ library provides basic message-passing, concurrency and choice, as well as integrated support for tracing. The ‘chp-plus’ library provides higher-level features such as process composition operators and behaviour combinators. This talk provides an introduction to the two libraries and the programming style they engender — as well as a brief look at the formal semantics underlying the libraries.Bio: Neil Brown is a software researcher from the University of Kent in the UK. After graduating he worked for several years as a machine learning researcher in industry at QinetiQ, before returning to university to undertake his PhD. He started out writing a Haskell-based compiler for synchronous message-passing languages, and ended up programming some synchronous message-passing libraries for Haskell itself. As well as these CHP libraries, he also developed the Progression benchmark-graphing library for Haskell. More detail on both projects can be found on his blog.

Read More

Tech Talk: Modern Benchmarking in Haskell

Details:

  • Title: Modern Benchmarking in Haskell (slides)
  • Presenter: Don Stewart
  • Date: Tuesday, 23 February 2010
  • Time: 10:30am
  • Location: Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

Abstract: Thanks to work by Bryan O’Sullivan, there has been a renaissance in performance benchmarking tools for Haskell, built upon Criterion.“Compared to most other benchmarking frameworks (for any programming language, not just Haskell), criterion focuses on being easy to use, informative, and robust.”Criterion uses statistically robust mechanisms for sampling and computing sound microbenchmark results, and is more stable in the presence of noise on the system than naive timings.Criterion has in turn spawned some extensions:

  • Progrssion: compare different criterion graphs
  • NoSlow: a new array benchmark suite based on Criterion

In this talk I will present these tools, how to use them, and how to make your performance benchmarks in Haskell, or languages Haskell can talk to, more reliable.Bio: Don is an Australian open source hacker, and engineer at Galois, Inc, in Portland, Oregon, where he works on creating trustworthiness and assurance in critical systems with an emphasis on language design and compiler techniques. Don is co-author of the book, Real World Haskell, published by O’Reilly, and the XMonad window manager.


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. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Read More

Tech Talk: Introduction to Aarne Ranta’s GF, the Grammatical Framework

The talk will be presented by Iavor Diatchki on Tuesday, February 16th, at 10:30am.(slides)Abstract: The Grammatical Framework (created by Aarne Ranta) is a programming language for multilingual grammar applications. It may be seen in a number of different ways:

  • as a special-purpose language for grammars, like YACC or Happy, but not restricted to programming languages;
  • as a functional language, like Haskell or SML, but specialized to grammar writing;
  • as a logical framework, like Agda or Coq, but equipped with concrete syntax in addition to logic;
  • as a natural language processing framework, like LKB, or Regulus, but based on functional programming and type theory.

This talk is an introduction to GF’s basic concepts by example. We will look at how to define the meaning and syntax of a language, perform simple translations, define semantic properties, and how to use GF together with another language such as Haskell.Bio: Iavor Diatchki is a R&D Engineer at Galois, Inc. with a Ph.D. from the Oregon Graduate Institute.Details:

  • Date: February 16th, 2010, Tuesday
  • Time: 10:30am
  • Location: Galois Inc., 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth building)

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. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Read More

Tech Talk: An Introduction to the Maude Formal Tool Environment

The talk will be presented by Joe Hendrix on Tuesday, February 2nd, at 10:30am. (slides)Abstract: There is a great deal of interest today in developing multi-purpose environments that combine declarative programming, with specification languages and useful automated analysis techniques. In this talk, I will survey one such an environment: the Maude system. I will start by describing how to program in Maude with a focus on its support for rewriting modulo axioms. After some examples, I will also survey some of the different analysis tools developed on top of the Maude system —- including the model checker, inductive theorem prover, and an extension to the core language for modeling systems that operate in real-time.Details:

  • Date: February 2nd, 2010, Tuesday
  • Time: 10:30am
  • Location: Galois Inc.,  421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth building)

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. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Read More

Tech Talk: A Scalable I/O Manager for GHC

The talk will be presented by Johan Tibell on Friday, January 29th, at 1:30pm. Slides are available (also on Slideshare and  Scribd).Abstract: The Glasgow Haskell Compiler supports extraordinarily cheap threads. These are implemented using a two-level model, with threads scheduled across a set of OS-level threads. Since the lightweight threads can’t afford to block when performing I/O operations, when a Haskell program starts, it runs an I/O manager thread whose job is to notify other threads when they can safely perform I/O.The I/O manager manages its file descriptors using the select system call. While select performs well for a small number of file descriptors, it doesn’t scale to a large number of concurrent clients, making GHC less attractive for use in large-scale server development.This talk will describe a new, more scalable I/O manager that’s currently under development and that hopefully will replace the current I/O manager in a future release of GHC.Details:

  • Date: January 29th, 2010, Friday
  • Time: 1:30pm
  • Location: Galois Inc.,  421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth building)

Bio: Johan Tibell is a Software Engineer at Google Inc. He received a M.S. in Software Engineering from the Chalmers University of Technology, Sweden, in 2007.


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. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Read More

Tech Talk: Ground Interpolation for Combined Theories

The next Galois Tech Talk will be delivered by Amit Goel.  Come kick off 2010 with us!Title: Ground Interpolation for Combined Theories Abstract: We give a method for modular generation of ground interpolants in modern SMT solvers supporting multiple theories. Our method uses a novel algorithm to modify the proof tree obtained from an unsatifiability run of the solver into a proof tree without occurrences of troublesome “uncolorable” literals. An interpolant can then be readily generated using existing procedures. The principal advantage of our method is that it places few restrictions (none for convex theories) on the search strategy of the solver. Consequently, it is straightforward to implement and enables more efficient interpolating SMT solvers. In the presence of non-convex theories our method is incomplete, but still more general than previous methods.

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

Bio: Amit Goel is a member of Intel’s Strategic CAD Labs.


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. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Read More

Tech Talk: John Launchbury presents Conal Elliott’s “Beautiful Differentiation”

The December 15th Galois Tech Talk will be delivered by John Launchbury.  He will present Conal Elliott’s 2009 ICFP paper entitled  Beautiful Differentiation for those of us who were not able to attend this wonderful talk in-person.

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

Abstract: Automatic differentiation (AD) is a precise, efficient, and convenient method for computing derivatives of functions. Its forward-mode implementation can be quite simple even when extended to compute all of the higher-order derivatives as well. The higher-dimensional case has also been tackled, though with extra complexity. This paper develops an implementation of higher-dimensional, higher-order, forward-mode AD in the extremely general and elegant setting of calculus on manifolds and derives that implementation from a simple and precise specification.In order to motivate and discover the implementation, the paper poses the question, “What does AD mean, independently of implementation?‚” An answer arises in the form of naturality of sampling a function and its derivative. Automatic differentiation flows out of this naturality condition, together with the chain rule. Graduating from first-order to higher-order AD corresponds to sampling all derivatives instead of just one. Next, the setting is expanded to arbitrary vector spaces, in which derivative values are linear maps. The specification of AD adapts to this elegant and very general setting, which even simplifies the development.Bio: John Launchbury is the founder and Chief Scientist of Galois, Inc.


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. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Read More

Tech Talk: Hoare-Logic – fiddly details and small print

[Note the Friday date, instead of the usual Tuesday slot.]The November 13th Galois Tech Talk will be delivered by Rod Chapman, titled Hoare-Logic – fiddly details and small print.”

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

Abstract: Hoare’s “assignment axiom” is noted for its simplicity and elegance, which seems to suggest that practical implementations are somehow “easy”. This talk will focus on our experience with SPARK – a programming language and toolset whose principal design goal is the provision of a sound Hoare-style verification system. I will concentrate on the “small print” and various fiddly (but essential) langauge features, such as volatility, I/O, dealing with commercial compilers, soundness and so on, that make the system much harder to implement than you might think.Bio: Rod Chapman is a Principal Engineer with Praxis, specializing in the design and implementation of safety and security-critical systems. He currently leads the development of the SPARK language and its associated analysis tools.Rod is a well-known conference speaker and has presented papers, tutorials, and workshops at many international events including SSTC, NSA HCSS, SIGAda, Ada-Europe and the Society of Automotive Engineers (SAE) World Congress. In addition to SPARK, Rod has been the key contributor to many of Praxis’ major projects such as SHOLIS, MULTOS CA, Tokeneer and Software verification tools. He received a MEng in Computer Systems and Software Engineering and a DPhil in Computer Science from the University of York, England, in 1991 and 1995 respectively. He is a Chartered Engineer, a Fellow of the British Computer Society, and also an SEI-Certified PSP Instructor.


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. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Read More