A. Gill and B. Neuenschwander, “Handshaking in Kansas Lava using patch logic,” in Practical Aspects of Declarative Languages, vol. 7149 of LNCS, Springer-Verlag, January 2012.



Designing hardware is like writing music for an orchestra - lots of pieces have to come together at the correct time for everything to work. In systems design, there is a confusing array of standards for allowing cooperating components, and little type-level support in traditional design methodologies for helping connect components with pre-arranged protocols. In this paper, we explore bringing protocol-level types to communicating processes. Inside our hardware description language Kansas Lava we introduce the notation of a patch, which is a communicating component with well-understood protocols. We build a theory round the notion of patches, which we call patch logic, and then use the patch abstraction to build a small driver for an FPGA board.


  title = {Handshaking in {K}ansas {L}ava using Patch Logic},
  author = {Andy Gill and Bowe Neuenschwander},
  booktitle = {Practical Aspects of Declarative Languages},
  publisher = {Springer-Verlag},
  series = {LNCS},
  volume = {7149},
  location = {Philadelphia, PA},
  year = {2012},
  month = {January},