Abstractions for the Functional Roboticist and A Taste of Agda

7pm: Blue Collar Abstractions for the Functional Roboticist
8pm: A Taste of Agda

----

7pm: Blue Collar Abstractions for the Functional Roboticist
Anthony Cowley

There are some constraints in this world that are hard. In robotics, we have literal names for the various considerations our software must accomodate: brick walls, gravity, ditches by the side of the road. The pressing need to avoid these pitfalls is confounded by traditional engineering approaches that seek to improve reliability by avoiding 'reinventing the wheel'. Sometimes you really do need a different wheel! Nonetheless, the industry at large leans toward the use of ever-larger prefabricated units of functionality designed to be used off the shelf. This high-level encapsulation of functionality grants power and reliability at the expense of flexibility.

In contrast, Haskell empowers those working on low-level programming by abstracting low-level functionality as well as high. Haskell's type system gives the programmer the confidence and ability to consider the parts from which complex software is assembled, swapping out pieces at any granularity. This power enables a new era of bespoke software that snugly fits the problem domain to which it is applied.

This talk will provide an overview of robotics research, examples of Haskell and GHC providing more expressive and efficient abstractions for existing architectures, and present the use of Haskell in real time perception for robotic systems.

• Anthony Cowley is a robotics researcher and PhD candidate at the GRASP Lab at the University of Pennsylvania. He has worked on video games for music education and entertainment, and was a research associate at GRASP before returning to student life in 2010. His interests are in real-time computer vision, embedded systems, multi-agent coordination, and programming language driven verification of robotic systems.

----

8pm: A Taste of Agda
Francesco Mazzoli

If you thought that Haskell was strongly typed, think again. Languages like Agda employ a type system embodying a very powerful logic, which lets us express the meaning of our programs much more precisely. Computers can understand our programs better too, allowing for tools that are more helpful than in average languages.

In this session we will interactively develop a type checker for a simple language, then give the language semantics by embedding it into Agda. This will allow us to prove a simple optimization on the language safe, by verifying that it preserves the meaning of programs.

• Francesco Mazzoli spent 4 years in London studying at Imperial College, where he met Haskell in his first lecture. In the past year he got interested in type theory and Agda in particular, focusing on the theme of equality for his masters’ thesis. He will soon start working at Erudify, an Haskell-backed company based in Zürich.