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 gamebased

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.

PDF file

In  Proceedings of the 15th ACM SIGPLAN international conference on Functional programming

Publisher  ACM

Details