A. Gill, T. Bull, A. Farmer, G. Kimmell, and E. Komp, “Types and associated type families for hardware simulation and synthesis: The internals and externals of Kansas Lava,” Journal of Higher-Order and Symbolic Computation, pp. 1–20, 2013.



In this article we overview the design and implementation of the second generation of Kansas Lava. Driven by the needs and experiences of implementing telemetry decoders and other circuits, we have made a number of improvements to both the external API and the internal representations used. We have retained our dual shallow/deep representation of signals in general, but now have a number of externally visible abstractions for combinatorial and sequential circuits, and enabled signals. We introduce these abstractions, as well as our abstractions for reading and writing memory. Internally, we found the need to represent unknown values inside our circuits, so we made aggressive use of associated type families to lift our values in a principled and regular way. We discuss this design decision, how it unfortunately complicates the internals of Kansas Lava, and how we mitigate this complexity. Finally, when connecting Kansas Lava to the real world, the standardized idiom of using named input and output ports is provided by Kansas Lava using a new monad, called \verb|Fabric|. We present the design of this Fabric monad, and illustrate its use in a small but complete example.


  issn = {1388-3690},
  journal = {Journal of Higher-Order and Symbolic Computation},
  doi = {10.1007/s10990-013-9098-7},
  publisher = {Springer US},
  keywords = {Domain specific languages; Hardware; Synthesis; Types},
  pages = {1-20},
  title = {Types and Associated Type Families for Hardware Simulation and Synthesis:
          The Internals and Externals of {K}ansas {L}ava},
  author = {Andy Gill and Tristan Bull and Andrew Farmer and Garrin Kimmell and Ed Komp},
  year = {2013},