In 2008-2010, I took a detour from my otherwise quite academic career into the mundane land of web portals, agreeing to a two-year contract for the Singtel Optus group. During that time, I designed and implemented a number of algorithmic solutions to their data mining and scalability problems, including a distributed and persistent real-time job scheduler intended for ingestion of data from error-prone external suppliers, and a duplication-preventing content allocation system for the Singapore inSing.com portal, based on the ideas from graph coloring-based register allocation.
Prior to my engagement at Optus, I spent three years at National ICT Australia (NICTA). As my first project at NICTA, I was entrusted with the task of developing from scratch a detailed and rigorous reference manual for the L4 microkernel, to replace the existing inadequate documentation of the system, as well as revamping the old inconsistent programming system interface for use in Qualcomm’s CDMA mobile chipsets. Subsequently, I joined the Potoroo project, which aimed to provide a detailed timing model of the L4 microkernel through a combination of empirical measurements coupled with an automated formal proof of completeness of measurement coverage. My role in the project was to design and implement the algorithm that derives the proof automatically from the measurements and a binary executable image of the kernel.
Choose life. Choose understanding. If cold hardware is a computer's body, then logic is its soul. The creator of body only begins to fathom the depths of the soul; so loose yourself in the adventure - dwell into the mind of the machine, the romance and passion of understanding what makes it think not tick. And if you don't find it all romantic, just bite into the lambdas with the rest of the Greek alphabet, enjoy the disorientating texture of theory in your mouth, have fun with the abstractions. Sounds crazy? Welcome to the PiLlS lab!
Here, in the dungeons of the University of New South Wales, for seven long years I said my prayers to the gods of logic; having taken the vows of (relative) poverty, chastity (from C), and obedience (to formal methods) some time in the second half of the Year of Our Lord 2003, I embarked on that narrow slippery road to knowledge that some call “doing a PhD”. By December 2009, under the patient guidance of Manuel M.T. Chakravarty, I have completed my research, providing humanity with this study in Haskell of purely-functional techniques for a formal specification of imperative programming languages and an epistemically-sound verification of their compilers. Oh beautiful, wise and strong goddess - Pallas Athena, thanks be to thee for your guidance through my quest!
Before I joined PilLS, I was hacking operating systems, hardware simulators and other such quick-and-dirty utilities together with other madmen from the DiSy (DiSy) Kernel Experimentation Group (KEG) lab at the University of New South Wales Computer Science & Engineering department. My original undergraduate thesis involved writing an L4 microkernel for the UltraSPARC architecture. If you don't know what L4, microkernel, UltraSPARC or an architecture is, you probably don't want to be enlightened, but just in case I'm wrong, I've provided links explaining all the gory details. Later on, I met Peter Strazdins from the Australian National University / Fujitsu CAP group who was just investigating porting of the SimOS system simulator to UltraSPARC. Since I've been tweaking with SimOS for some time, the L4 thesis got scratched and Sulima was born.
I commenced my study at the University of New South Wales in 1996, mostly at the School Computer Science & Engineering, although in 1997-1999 I took a brief detour into the area of philosophy (mostly methaphysics and epistemology.) Eventually, I graduated in 2000, with an honors thesis on The Design and Implementation of an Extendible Instruction Set Simulators. I continued my post-graduate study, also at UNSW, on the application of purely functional languages in compilation and verification of imperative programming environments, eventually completing my PhD in 2011.