Practicality! Reflex: Practical FRP and Making Dependent Types Practical
Details
As usual, we will be meeting at Akamai from 7-9pm.
7:00-8:00: Ryan Trinkle - Reflex: Practical Functional Reactive Programming
Ryan Trinkle presents his new library, Reflex, a deterministic, efficient, higher-order Functional Reactive Programming system. FRP is a radically new paradigm for writing interactive software: Instead of writing event loops or callbacks, programmers compose interactive applications using ordinary pure functional programming methods. The unique design of Reflex gives it the power and flexibility necessary to handle complex large-scale applications. Reflex can be compiled to binary using GHC or JavaScript using GHCJS.
8:00-9:00: Chris Casinghino - Making Dependent Types Practical
The last decade has seen many success stories for verified programming with dependent types, including the CompCert verified C compiler, verified libraries for concurrency and security, and machine-checked proofs of results like the four color theorem and the Feit-Thompson theorem. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. In this talk, I’ll describe several limitations of modern dependently-typed languages that are holding them back from wider adoption for practical programming tasks. I’ll explain the historical and mathematical reasons for these limitations, and describe how we attempted to relax them in the design of the Zombie research language.
Speaker Bios:
Ryan Trinkle:
Ryan Trinkle has been CTO of a successful Haskell-based startup, founder of an exclusively-Haskell software development company, and co-founder of the New York Haskell Meetup.
Chris Casinghino:
Chris Casinghino is a Senior Member of the Technical Staff at Draper Laboratory, where he develops static analysis tools in Haskell. In 2014, he completed a PhD in the programming languages group at The University of Pennsylvania. His research focuses on dependently typed programming languages, exploring both their semantics and how to use them to write better programs.
Logistics:
If you can, please plan on arriving between 6:45pm and 7pm, but there will be someone in the lobby to greet stragglers.
Food:
Pizzas, salad and soda.
Afterwards:
If you'd like to stick around, a number of us tend to head down to the CBC (http://www.cambrew.com/) or another pub afterwards to socialize. If you would like to give a talk or if you have any questions or concerns, please feel free to follow up here or email one of the organizers.