{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:45Z","timestamp":1779836745664,"version":"3.53.1"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2012,8,15]],"date-time":"2012-08-15T00:00:00Z","timestamp":1344988800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2012,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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\u2013answer 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 \u03bb-calculus with polymorphic constants. 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. Formal properties of the framework have been proved using the Coq proof assistant.<\/jats:p>","DOI":"10.1017\/s0956796812000263","type":"journal-article","created":{"date-parts":[[2012,8,15]],"date-time":"2012-08-15T08:45:18Z","timestamp":1345020318000},"page":"529-573","source":"Crossref","is-referenced-by-count":9,"title":["Every bit counts: The binary representation of typed data and programs"],"prefix":"10.1017","volume":"22","author":[{"given":"ANDREW J.","family":"KENNEDY","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DIMITRIOS","family":"VYTINIOTIS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2012,8,15]]},"reference":[{"key":"S0956796812000263_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2088456.1863525"},{"key":"S0956796812000263_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005209"},{"key":"S0956796812000263_ref30","first-page":"237","volume-title":"Selected Papers from the International Workshop on Types for Proofs and Programs (TYPES '06)","author":"Sozeau","year":"2006"},{"key":"S0956796812000263_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277752"},{"key":"S0956796812000263_ref5","first-page":"550","volume-title":"DCC '00: Proceedings of the Conference on Data Compression","author":"Cheney","year":"2000"},{"key":"S0956796812000263_ref31","first-page":"53","volume-title":"ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI)","author":"Sulzmann","year":"2007"},{"key":"S0956796812000263_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/844102.844114"},{"key":"S0956796812000263_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1982595.1982615"},{"key":"S0956796812000263_ref19","first-page":"209","volume-title":"Proceedings of the 8th International Conference on Mathematics of Program Construction, MPC06, volume 4014 of LNCS","author":"Holdermans","year":"2006"},{"key":"S0956796812000263_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291199"},{"key":"S0956796812000263_ref33","first-page":"41","volume-title":"Proceedings of the 5th Int'l Conference on Approaches and Applications of Inductive Programming (AAIP)","author":"Yakushev","year":"2009"},{"key":"S0956796812000263_ref13","unstructured":"Franz M. , Haldar V. , Krintz C. & Stork C. H. (2002) Tamper-Proof Annotations by Construction. Tech. Rep. 02-10. Department of Information and Computer Science, University of California, Irvine."},{"key":"S0956796812000263_ref7","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380150702"},{"key":"S0956796812000263_ref4","doi-asserted-by":"publisher","DOI":"10.1109\/18.9782"},{"key":"S0956796812000263_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0956796812000263_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55611-7"},{"key":"S0956796812000263_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84800-072-8"},{"key":"S0956796812000263_ref10","volume-title":"Standard ECMA-335: Common Language Infrastructure (CLI)","year":"2006"},{"key":"S0956796812000263_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21254-3_32"},{"key":"S0956796812000263_ref32","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/1863543.1863548","volume-title":"ACM SIGPLAN International Conference on Functional Programming (ICFP)","author":"Vytiniotis","year":"2010"},{"key":"S0956796812000263_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_36"},{"key":"S0956796812000263_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360216"},{"key":"S0956796812000263_ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1975.1055349"},{"key":"S0956796812000263_ref29","volume-title":"Lectures on the Curry-Howard Isomorphism (Studies in Logic and the Foundations of Mathematics, Volume 149)","author":"S\u00f8rensen","year":"2006"},{"key":"S0956796812000263_ref18","unstructured":"Hinze R. , Jeuring J. & L\u00f6h A. (2006) Comparing approaches to generic programming in Haskell. Spring Sch. Datatype-Generic Program, LNCS, vol. 4719, pp. 72\u2013149."},{"key":"S0956796812000263_ref14","first-page":"1","article-title":"Representations of stream processors using nested fixed points","volume":"5","author":"Ghani","year":"2009","journal-title":"Logical Methods Comput. Sci."},{"key":"S0956796812000263_ref22","volume-title":"Information Theory, Inference and Learning Algorithms","author":"MacKay","year":"2003"},{"key":"S0956796812000263_ref16","unstructured":"Gonthier G. , Mahboubi A. & Tassi E. (2011) A Small Scale Reflection Extension for the Coq System. Tech. Rep. 6455. INRIA."},{"key":"S0956796812000263_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"S0956796812000263_ref3","volume-title":"Proceedings of the USENIX Conference on Web Application Development","author":"Burtscher","year":"2010"},{"key":"S0956796812000263_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1111320.1111039"},{"key":"S0956796812000263_ref15","first-page":"1","volume-title":"Datatype-Generic Programming","author":"Gibbons","year":"2007"},{"key":"S0956796812000263_ref2","first-page":"1","volume-title":"Advanced Functional Programming 4","author":"Bird","year":"2003"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796812000263","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:27Z","timestamp":1779834987000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796812000263\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,15]]},"references-count":33,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2012,9]]}},"alternative-id":["S0956796812000263"],"URL":"https:\/\/doi.org\/10.1017\/s0956796812000263","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,15]]}}}