Andrew Kennedy: Publications on Functional Programming

"I do not believe in object-oriented programming."

Publications

Every Bit Counts: The binary representation of typed data and programs
Andrew Kennedy and Dimitrios Vytiniotis. Journal of Functional Programming (JFP), 2012, to appear.

We show how the binary encoding and decoding of typed data and typed programs can be understood, programmed, and verified with the help of question-answer games. The encoding of a value is determined by the yes/no answers to a sequence of questions about that value; conversely, decoding is the interpretation of binary data as answers to the same question scheme. We introduce a general framework for writing and verifying game-based codecs. We present games in Haskell for structured, recursive, polymorphic, and indexed types, building up to a representation of well-typed terms in the simply-typed lambda-calculus with polymorphic constants. The framework makes novel use of isomorphisms between types in the de nition of games. The de nition of isomorphisms together with additional simple properties make it easy to prove that codecs derived from games never encode two distinct values using the same code, never decode two codes to the same value, and interpret any bit sequence as a valid code for a value or as a prefix of a valid code. Formal properties of the framework have been proved using the Coq proof assistant.

Functional Pearl: Every Bit Counts
Dimitrios Vytiniotis and Andrew Kennedy. International Conference on Functional Programming (ICFP), September 2010, Baltimore, Maryland, US.

We show how the binary encoding and decoding of typed data and typed programs can be understood, programmed, and verified with the help of question-answer games. The encoding of a value is determined by the yes/no answers to a sequence of questions about that value; conversely, decoding is the interpretation of binary data as answers to the same question scheme. We introduce a general framework for writing and verifying game-based codecs. We present games for structured, recursive, polymorphic, and indexed types, building up to a representation of well-typed terms in the simply-typed lambda-calculus. The framework makes novel use of isomorphisms between types in the definition of games. The definition of isomorphisms together with additional simple properties make it easy to prove that codecs derived from games never encode two distinct values using the same code, never decode two codes to the same value, and interpret any bit sequence as a valid code for a value or as a prefix of a valid code.

Functional Pearls: Drawing Trees
Andrew Kennedy. Journal of Functional Programming, 6(3): 527-534, Cambridge University Press, May 1996.

This article describes the application of functional programming techniques to a problem previously studied by imperative programmers, that of drawing general trees automatically. We first consider the nature of the problem and the ideas behind its solution (due to Radack), independent of programming language implementation. We then describe a Standard ML program which reflects the structure of the abstract solution much better than an imperative language implementation. We conclude with an informal discussion on the correctness of the implementation and some changes which improve the algorithm's worst-case time complexity.

Functional Pearls: Pickler Combinators
Andrew Kennedy. Journal of Functional Programming, special issue on Functional Pearls, 14(6): 727-739, Cambridge University Press, Nov 2004.

The tedium of writing pickling and unpickling functions by hand is relieved using a combinator library similar in spirit to the well-known parser combinators. Picklers for primitive types are combined to support tupling, alternation, recursion, and structure sharing. Code is presented in Haskell; an alternative implementation in ML is discussed.