Computer Scientist with skills in formal verification and theorem proving (e.g Agda and Isabelle/HOL) as well as functional programming, particularly Haskell. Software engineer with abilities in all industry languages and frameworks (Java, .NET) as well as languages popular in emerging technologies such as Erlang, Scala and Ruby.
Extensive experience in web development, including experience at Google in the development of a new product (Google Wave). Follows closely development of new standards for the Web.
Extensive experience with concurrent and distributed programmming, aware of various approaches to concurrency abstraction and concurrent data structures. Able to structure constructive proofs of properties on concurrent programs using standard methods.
Solid understanding of common formal verification tools and how to structure proofs of termination, deadlock-freedom, and various liveness properties.
Extensive experience with formal semantics of programming languages, particularly in the encoding of logic into language type systems, and the use of this as a proof method via the Curry Howard correspondence.
An active member of the Haskell community and author of many open source libraries. My research often involves this language.
Has a moderate understanding of conversational Japanese and can read and write at a rudimentary level, and beginning study of Vietnamese.
Functional Programming; Formal Verification; Type Theory; Logic; Logic Programming; Programming Languages; Compilers; Web Development; Category Theory; Discrete Mathematics; Theorem Proving; Parallelism; Concurrency; Distributed Computing.
Agda, Haskell, OCaml, Ruby, Scala, Java, C#, C, F#, JavaScript (+jQuery), Scheme
C++, Python, Perl 5, Perl 6, haXe, Lua, Go, Assembly (x86, ARM, AVR), Isabelle/HOL
Coq, Prolog, Mercury
April 2011 - Present
Working on improvements to the L4.verified project, the first formally verified, proven correct operating system. Real-world code with formal rigor and verification.
January 2009 - Present
Responsible for the teaching of classes and consultations, marking assignments, and so on. I have taught Computing 1A, Higher Data Structures and Algorithms, Engineering Design in Computing, (Formal) Concepts of Programming Languages, and Software System Design and Implementation, a course involving theorem proving with the Agda proof checker.
August 2010 - March 2011
Developing a web application for travellers to share information with each other. Developed using Haskell web frameworks (Yesod) and a RESTful API.
November 2009 - March 2010
Experience working with a large team and practicing Agile methods. Worked in Java and Google Web Toolkit for the development of client-side features on Google/Apache Wave.
November 2008 - October 2009
Experience working on a facebook application with Ruby and JavaScript frameworks.
July 2005 - May 2008
Experience in development tools and work flows, while operating my own startup development business. Currently suspended operations due to research priorities.