Jon
Jon is a PhD student at Carnegie Mellon University studying type theory and categorical logic, and is also the creator of the RedPRL proof assistant.
Darin
Darin is a former grad student who studied dependent type theory and programming languages at the University of Nottingham.
David
David works in industry. He is co-author of The Little Typer and a contributor to the Idris project.