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

The University of Illinois at Chicago

Department of Computer Science

Advanced Programming Seminar

Demonstrating Agda

Alan Jeffrey

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 programs and pure functional GUIs. He is the author of the JavaScript back end for Agda.

Copyright 2016 The Board of Trustees
of the University of
Helping Women Faculty Advance
Funded by NSF