Show simple item record

dc.rights.licenseCC-BY-NC-ND
dc.contributor.advisorSwierstra, dr. W. S.
dc.contributor.authorPizani Flor, J.P.
dc.date.accessioned2014-09-16T17:01:05Z
dc.date.available2014-09-16T17:01:05Z
dc.date.issued2014
dc.identifier.urihttps://studenttheses.uu.nl/handle/20.500.12932/18341
dc.description.abstractRecently, the incentives for hardware acceleration of algorithms are growing, as Moore's law continues to hold but optimizations in traditional processors show diminishing returns. This growing need for hardware implementation pushes programmers towards hardware design, an activity with stricter correctness and performance requirements than software development. A long-standing line of research is concerned with the application of functional programming techniques to hardware design, and the relatively recent dependently-typed programming paradigm has been claimed by many researchers to be the "successor" of functional programming. This thesis aims, therefore, to investigate what are the improvements that Dependently-Typed Programming (DTP) can bring to hardware design. We developed a domain-specific language for hardware, called Π-Ware, embedded as a library in the Agda programming language. Π-Ware allows the specification of circuits, their simulation, synthesis and verification. Compared to similar approaches in the literature, Π-Ware provides high type safety and robust proofs of correctness for whole families of circuits, however it still needs significant improvements in terms of ease-of-use.
dc.description.sponsorshipUtrecht University
dc.format.extent470036
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.titlePi-Ware: An Embedded Hardware Description Language using Dependent Types
dc.type.contentMaster Thesis
dc.rights.accessrightsOpen Access
dc.subject.keywordsEDSL, HDL, Hardware Description, Functional Programming, Dependent types, Agda, Coq, Lava, Coquet
dc.subject.courseuuComputing Science


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record