# Π-Ware

An Embedded Hardware Description Language using Dependent Types.

This wiki describes the Π-Ware project, begun in mid-2014 as the thesis project of my M.Sc programme
at Utrecht University. Π-Ware is an Embedded Domain-Specific Language (EDSL) for hardware design,
packaged as a library for the Agda programming language.
It uses the power of dependent types in order to *ban* certain classes of design mistakes *by construction*,
which means that trying to model a *malformed* circuit will result in a *type error*.
Also, due to being embedded in Agda, *proofs* concerning Π-Ware circuit models can be written
in the same language as the the models themselves.

There is a GitHub repository containing **only**
the Agda source code of the library.
If you are interested in looking at the M.Sc thesis's text and figures,
or some presentations given about Π-Ware, you can go to the
general Π-Ware repository,
which contains all code **and** documentation related to the project.

Here in the wiki you can find information about how the library is structured,
examples of how to model circuits and some examples of proofs of circuit properties.
Specific instructions on how to install and use the Π-Ware library can be found
in the `README`

file of the library's source code repository.

## Pages

### Proposal

Consists of a very high-level description of the project's goals, in the period between March and August 2014.

### Literature

This page lists technologies and research related to the questions addressed in the project. There are also some reviews of the literature consulted.

### Planning

### Library / Usage

Pages detailing the inner workings of the Π-Ware library, and justifying some of the design decisions taken. Some simple examples of Π-Ware circuit models and proofs.