Research Buffet
Wednesday, November 2, 2011
3147 MEB
Lecture 4:00 p.m.
Phillip Mates
Title: Higher Order Types for Fun and Profit
Wednesday, November 2, 2011
3147 MEB
Lecture 4:00 p.m.
Phillip Mates
Title: Higher Order Types for Fun and Profit
Abstract
On the surface, types are yet another talisman to help ward off evil run-time errors and ensure program correctness. Unbeknownst to most is the fact that type systems for functional languages have a direct correspondence to the intuitionistic subset of classical logic. This correspondence, known as the Curry-Howard Isomorphism, has led to many novel program language implementations and continues to yield interesting results.
In this talk I will give an introduction to intuitionistic logic, simply typed lambda calculus, and show how the Curry-Howard Isomorphism holds between them. Furthermore, I will explore higher order type systems that leverage the Curry-Howard Isomorphism, such as polymorphic lambda calculus and types that depend on values. Lastly I will show how the Isomorphism might be used to further the relatively new field of program synthesis.
Kathryn Rodgers
Title: Parallel Compression of Time-Variant Scientific Data for Collaborative Visualizations
On the surface, types are yet another talisman to help ward off evil run-time errors and ensure program correctness. Unbeknownst to most is the fact that type systems for functional languages have a direct correspondence to the intuitionistic subset of classical logic. This correspondence, known as the Curry-Howard Isomorphism, has led to many novel program language implementations and continues to yield interesting results.
In this talk I will give an introduction to intuitionistic logic, simply typed lambda calculus, and show how the Curry-Howard Isomorphism holds between them. Furthermore, I will explore higher order type systems that leverage the Curry-Howard Isomorphism, such as polymorphic lambda calculus and types that depend on values. Lastly I will show how the Isomorphism might be used to further the relatively new field of program synthesis.
Kathryn Rodgers
Title: Parallel Compression of Time-Variant Scientific Data for Collaborative Visualizations
Abstract
Research is becoming increasingly dependent on visual aides to display results and analyze experiments. However, the size of the data set required to render these visualizations can limit researchers' abilities to share results or collaborate with distant peers. My research focuses on creating algorithms to quickly compress these data sets into manageable sizes so that they can be distributed more easily. The work is based on parallelizing existing compression algorithms specific to time-variant scientific data that uses a series of points' paths to render an image. These methods include a Trajectory Simplification method and a Cluster Simplification method. These methods have been recreated as parallel algorithms so that they run as much as seven times faster than the originals.
Research is becoming increasingly dependent on visual aides to display results and analyze experiments. However, the size of the data set required to render these visualizations can limit researchers' abilities to share results or collaborate with distant peers. My research focuses on creating algorithms to quickly compress these data sets into manageable sizes so that they can be distributed more easily. The work is based on parallelizing existing compression algorithms specific to time-variant scientific data that uses a series of points' paths to render an image. These methods include a Trajectory Simplification method and a Cluster Simplification method. These methods have been recreated as parallel algorithms so that they run as much as seven times faster than the originals.