March 14, 2012: Advanced Programming Seminar - Alan Jeffrey: "Demonstrating Agda"
The University of Illinois at Chicago
Department of Computer Science
Advanced Programming Seminar
Wednesday, March 14, 2012
12:00 p.m., Room 1000 SEO
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.
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
back end for Agda.