License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2015.9
URN: urn:nbn:de:0030-drops-84791
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8479/
Go to the corresponding LIPIcs Volume Portal

Pizani Flor, João Paulo ; Swierstra, Wouter ; Sijsling, Yorick

Pi-Ware: Hardware Description and Verification in Agda

pdf-format:
LIPIcs-TYPES-2015-9.pdf (0.7 MB)

Abstract

There is a long tradition of modelling digital circuits using functional programming languages. This paper demonstrates that by employing dependently typed programming languages, it becomes possible to define circuit descriptions that may be simulated, tested, verified and synthesized using a single language. The resulting domain specific embedded language, Pi-Ware, makes it possible to define and verify entire families of circuits at once. We demonstrate this by defining an algebra of parallel prefix circuits, proving their correctness and further algebraic properties.

BibTeX - Entry

@InProceedings{pizaniflor_et_al:LIPIcs:2018:8479,
  author =	{Jo{\~a}o Paulo Pizani Flor and Wouter Swierstra and Yorick Sijsling},
  title =	{{Pi-Ware: Hardware Description and Verification in Agda}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{9:1--9:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Tarmo Uustalu},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8479},
  URN =		{urn:nbn:de:0030-drops-84791},
  doi =		{10.4230/LIPIcs.TYPES.2015.9},
  annote =	{Keywords: dependently typed programming, Agda, EDSL, hardware description languages, functional programming}
}

Keywords: dependently typed programming, Agda, EDSL, hardware description languages, functional programming
Collection: 21st International Conference on Types for Proofs and Programs (TYPES 2015)
Issue Date: 2018
Date of publication: 15.03.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI