Talks and Presentations

Computers, Programs and Logic or What does Linux Prove? Presented at the Australian Linux Conference held in Sydney, Australia (January 2007.)

This talk is about hacking mathematics. I will try to give you guys an intuition behind formal logic and some cool things such as Curry-Haward isomorphism and Godel's incompletness theorem. I will show you what theorem proving is all about and why every one of you who has ever run GCC has already done plenty of theorem proving in their lives. This is not, however, a formal talk, and I've skipped a lot of details to make the material penetrable to an average l33t C hacker, so please don't shoot me if you know about this stuff and notice little lies in my talk. There's a few of them, but the basic idea is that, at the end, you will be able to go on Google (Wikipedia comes highly recommended!) search for all this stuff and find out all the nitty-gritty details for yourself. A few years ago I've attended a talk by Philip Wadler and, I've been using formal systems for years back then, but only during that talk Philip mentioned some insignificant thing about encoding of falsehood and it all “clicked together”: I got a zen-like light hit me from above and everything was clear and simple and beautiful. So I'm hoping this talk will give some of you a similar effect; the rest of you better have some panadols in your conference bags, because tonight you'll be nursing a massive hangover - and I don't mean from the conference dinner.

The Lost Art of Techno-masochism, or Hacking in TEX Presented at the Australian Linux Conference held in Adelaide, Australia (January 2004.)

It is well-known that the document typesetting system TEX is a Turing-complete language, and, as such, may be used to solve arbitriary programming problems. Many TEX users who have been exposed to the design of LaTEX packages even realise that hacking in TEX may be useful. It is a well-kept secret of the TEX elite (TEXperts) that it is also a lot of fun.

It is the purpose of this paper to explain the mechanics of using conventional programming structures in TEX, while exposing the utility of writing TEX programs, in a hope of initiating a few of its readers into the inner circle of TEX addicts.

The author of this paper has written a number of TEX programs himself, including K-Fish and lambdaTEX, a popular pretty-printing package for the functional language Haskell, written entirely in over 3000 lines TEX code. By working directly in TEX, lambdaTEX allows authors to incorporate neatly-typeset fragments of programs in LaTEX documents simply by pasting the code into an appropriate \begin{}..\end{} environment block, without resorting to any external preprocessing tools or heavy manual annotations, or putting up with the ugliness of code typset with the verbatim environment.

The indented audience of this paper are UNIX programmers who: (1) enjoy hacking and (2) use TEX or LaTEX to typeset technical papers containing programming code and (3) really, truly love hacking.

Few people realise that, from the language-theoretic point of view, TEX belongs to the lazy continuation-passing family of programming languages, which includes a few other popular languages such as Standard ML, Lisp and Scheme. Continuation passing style (CPS) has been successfully employed in the theoretical computer science community to model and implement sophisticated language features such as exceptions and concurrency. In C, a primitive form of CPS is available in the form of setjmp and longjmp. The paper explains this style of programming in terms that should be comprehendible to any competent hacker, even without a prior background in functional or declarative languages.

Once the continuation-passing style is understood, it is a small step to move from coding in ML to writing programs in TEX, and this paper will demonstrate how to make this step without requiring any prior knowledge of lambda calculus or functional programming.

Last but not least, it is a purpose of this paper to cultivate the old tradition of minimalistic hacking - doing the impossible with seemingly-inadequate tools, and, most importantly, having lots of fun in the process. In today's climate of a commercialization of the open source, it is worthwhile to look back to the days gone by, when public software was created only by hackers having fun over a cup of coffee.

From Assembly Language To Lambda Calculus or How to Trick a FORTRAN Hacker Into Writing a Functional Program Presented at a meeting of of the International Federation of Information Processing (IFIP) Working Group 2.8 on Functional Programming held in Coffs Harbour, Australia (December 2003.) Slides
SSA, CPS, ANF: Three Approaches to Compiling Functional Languages Presented at a meeting of the Programming Languages and Systems Group from the University of New South Wales, held in Sydney, Australia (November 2003.) Slides
Value Range Propagation in LLVM Presented at a meeting of the Programming Languages and Systems Group from the University of New South Wales, held in Sydney, Australia (October 2003.) Slides
What on Earth is Open Source? Observations from the Joint European Conferences on Theory and Practice of Software held in Warsaw, April 2003 Presented at a meeting of the Australian UNIX Users Group (AUUG) held in Sydney, Australia (July 2003.) Slides
Intermediate Program Representations for Register Allocation Presented at a meeting of the Programming Languages and Systems Group from the University of New South Wales held in Sydney, Australia (June 2003.) Slides
ETAPS 2003 Report Presented at a meeting of the Programming Languages and Systems Group from the University of New South Wales, held in Sydney, Australia (May 2003.) Slides
A Functional Perspective on SSA Optimization Algorithms Presented at the Workshop on Compilers Optimisations Meets Compiler Verification (COCV '03) held in Warsaw, Poland (April 2003.)

The static single assignment (SSA) form is central to a range of optimisation algorithms relying on data flow information, and hence, to the correctness of compilers employing those algorithms. It is well known that the SSA form is closely related to lambda terms (i.e., functional programs) and, considering the large amount of energy expended on theories and frameworks for formal reasoning in the lambda calculus, it seems only natural to leverage this connection to improve our capabilities to reason about compiler optimisations. In this paper, we discuss a new formalisation of the mapping from SSA programs to a restricted form of lambda terms, called administrative normal form (ANF). We conjecture that this connection improves our ability to reason about SSA-based optimisation algorithms and provide a first data point by presenting an ANF variant of a well known SSA-based conditional constant propagation algorithm.

Slides More