March 14, 2012: Advanced Programming Seminar - Alan Jeffrey: "Demonstrating Agda"

Abstract:

Agda is a functional programming language in the style of Haskell, but with a number of additional features. There is a termination checker which can ensure functions calls will always return, an emacs mode which supports iterative development of programs with holes, and a dependent type system which removes the distinction between types and programs. In this seminar, I will give a demonstration of Agda, and show how these features can be used to provide safety guarantees for programs which extend beyond simple memory safety into maintaining more complex code invariants.

Bio:

Alan Jeffrey is a Member of Technical Staff at Bell Labs. His research areas include programming languages, semantics, and security. He has investigated pragmatic uses of dependent types, including work on authenticity in cryptographic protocols, streaming I/O, reactive programs and pure functional GUIs. He is the author of the JavaScript back end for Agda.