Search Results

Documents authored by de Muijnck-Hughes, Jan

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.8
Wiring Circuits Is Easy as {0,1,ω}, or Is It...

Authors: Jan de Muijnck-Hughes and Wim Vanderbauwhede

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Quantitative Type-Systems support fine-grained reasoning about term usage in our programming languages. Hardware Design Languages are another style of language in which quantitative typing would be beneficial. When wiring components together we must ensure that there are no unused ports, dangling wires, or accidental fan-ins and fan-outs. Although many wire usage checks are detectable using static analysis tools, such as Verilator, quantitative typing supports making these extrinsic checks an intrinsic aspect of the type-system. With quantitative typing of bound terms, we can provide design-time checks that all wires and ports have been used, and ensure that all wiring decisions are explicitly made, and are neither implicit nor accidental. We showcase the use of quantitative types in hardware design languages by detailing how we can retrofit quantitative types onto SystemVerilog netlists, and the impact that such a quantitative type-system has when creating designs. Netlists are gate-level descriptions of hardware that are produced as the result of synthesis, and it is from these netlists that hardware is generated (fabless or fabbed). First, we present a simple structural type-system for a featherweight version of SystemVerilog netlists that demonstrates how we can type netlists using standard structural techniques, and what it means for netlists to be type-safe but still lead to ill-wired designs. We then detail how to retrofit the language with quantitative types, make the type-system sub-structural, and detail how our new type-safety result ensures that wires and ports are used once. Our ideas have been proven both practically and formally by realising our work in Idris2, through which we can construct a verified language implementation that can type-check existing designs. From this work we can look to promote quantitative typing back up the synthesis chain to a more comprehensive hardware description language; and to help develop new and better hardware description languages with quantitative typing.
Cite as

Jan de Muijnck-Hughes and Wim Vanderbauwhede. Wiring Circuits Is Easy as {0,1,ω}, or Is It.... In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 8:1-8:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{demuijnckhughes_et_al:LIPIcs.ECOOP.2023.8,
  author =	{de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
  title =	{{Wiring Circuits Is Easy as \{0,1,\omega\}, or Is It...}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{8:1--8:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.8},
  URN =		{urn:nbn:de:0030-drops-182010},
  doi =		{10.4230/LIPIcs.ECOOP.2023.8},
  annote =	{Keywords: Hardware Design, Linear Types, Dependent Types, DSLs, Idris, SystemVerilog, Netlists}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.4
Wiring Circuits Is Easy as {0, 1, ω}, or Is It... (Artifact)

Authors: Jan de Muijnck-Hughes and Wim Vanderbauwhede

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
We present two proof-of-concept languages (Circuits & CirQTS) that showcases how fancy types (namely linear & dependent types) can enrich hardware design tooling such that we can move existing external static analysis checks into the language’s type-system. Using our approach will lead to the enhanced safety of designs, and increase in design productivity, through early identification and reduction of connection errors. This artefact presents our verified implementations (as realised in Idris2) of the simply (Circuits) and fancily typed (CirQTS) languages, and the test suite used to assess efficacy of our approach.
Cite as

Jan de Muijnck-Hughes and Wim Vanderbauwhede. Wiring Circuits Is Easy as {0, 1, ω}, or Is It... (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{demuijnckhughes_et_al:DARTS.9.2.4,
  author =	{de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
  title =	{{Wiring Circuits Is Easy as \{0, 1, \omega\}, or Is It... (Artifact)}},
  pages =	{4:1--4:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.4},
  URN =		{urn:nbn:de:0030-drops-182442},
  doi =		{10.4230/DARTS.9.2.4},
  annote =	{Keywords: Hardware Design, Linear Types, Dependent Types, DSLs, Idris, SystemVerilog, Netlists}
}
Document
DOI: 10.4230/OASIcs.EVCS.2023.9
Type Theory as a Language Workbench

Authors: Jan de Muijnck-Hughes, Guillaume Allais, and Edwin Brady

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Language Workbenches offer language designers an expressive environment in which to create their Domain Specific Languages (DSLs). Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes! We have developed an exemplar DSL called Vélo that showcases not only dependently typed techniques to realise and manipulate Intermediate Representations (IRs), but that dependently typed languages make fine language workbenches. Vélo is a simple verified language with well-typed holes and comes with a complete compiler pipeline: parser, elaborator, REPL, evaluator, and compiler passes. Specifically, we describe our design choices for well-typed IR design that includes support for well-typed holes, how CSE is achieved in a well-typed setting, and how the mechanised type-soundness proof for Vélo is the source of the evaluator.
Cite as

Jan de Muijnck-Hughes, Guillaume Allais, and Edwin Brady. Type Theory as a Language Workbench. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 9:1-9:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{demuijnckhughes_et_al:OASIcs.EVCS.2023.9,
  author =	{de Muijnck-Hughes, Jan and Allais, Guillaume and Brady, Edwin},
  title =	{{Type Theory as a Language Workbench}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{9:1--9:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.9},
  URN =		{urn:nbn:de:0030-drops-177797},
  doi =		{10.4230/OASIcs.EVCS.2023.9},
  annote =	{Keywords: dependent types, language workbenches, idris2, dsl, edsl, intrinsically scoped, well typed, co-De Bruijn}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.2
A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact)

Authors: Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Idris' Effects library demonstrates how to embed resource dependent algebraic effect handlers into a dependently typed host language, providing run-time and compile-time based reasoning on type-level resources. Building upon this work, Resources is a framework for realising Embedded Domain Specific Languages (EDSLs) with type systems that contain domain specific substructural properties. Differing from Effects, Resources allows a language’s substructural properties to be encoded within type-level resources that are associated with language variables. Such an association allows for multiple effect instances to be reasoned about autonomically and without explicit type-level declaration. Type-level predicates are used as proof that the language’s substructural properties hold. Several exemplar EDSLs are presented that illustrates our framework’s operation and how dependent types provide correctness-by-construction guarantees that substructural properties of written programs hold.
Cite as

Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede. A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{demuijnckhughes_et_al:DARTS.6.2.2,
  author =	{de Muijnck-Hughes, Jan and Brady, Edwin and Vanderbauwhede, Wim},
  title =	{{A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact)}},
  pages =	{2:1--2:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{de Muijnck-Hughes, Jan and Brady, Edwin and Vanderbauwhede, Wim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.2},
  URN =		{urn:nbn:de:0030-drops-131995},
  doi =		{10.4230/DARTS.6.2.2},
  annote =	{Keywords: Dependent Types, Algebraic Effect Handlers, Domain-Specific Languages, Embedded Domain Specific Languages, Idris, Substructural Type-Systems}
}
Document
Pearl
DOI: 10.4230/LIPIcs.ECOOP.2020.20
A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Pearl)

Authors: Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Idris' Effects library demonstrates how to embed resource dependent algebraic effect handlers into a dependently typed host language, providing run-time and compile-time based reasoning on type-level resources. Building upon this work, Resources is a framework for realising Embedded Domain Specific Languages (EDSLs) with type systems that contain domain specific substructural properties. Differing from Effects, Resources allows a language’s substructural properties to be encoded within type-level resources that are associated with language variables. Such an association allows for multiple effect instances to be reasoned about autonomically and without explicit type-level declaration. Type-level predicates are used as proof that the language’s substructural properties hold. Several exemplar EDSLs are presented that illustrates our framework’s operation and how dependent types provide correctness-by-construction guarantees that substructural properties of written programs hold.
Cite as

Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede. A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Pearl). In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 20:1-20:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{demuijnckhughes_et_al:LIPIcs.ECOOP.2020.20,
  author =	{de Muijnck-Hughes, Jan and Brady, Edwin and Vanderbauwhede, Wim},
  title =	{{A Framework for Resource Dependent EDSLs in a Dependently Typed Language}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{20:1--20:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.20},
  URN =		{urn:nbn:de:0030-drops-131773},
  doi =		{10.4230/LIPIcs.ECOOP.2020.20},
  annote =	{Keywords: Dependent Types, Algebraic Effect Handlers, Domain-Specific Languages, Embedded Domain Specific Languages, Idris, Substructural Type-Systems}
}
Document
Artifact
DOI: 10.4230/DARTS.5.2.14
A Typing Discipline for Hardware Interfaces (Artifact)

Authors: Jan de Muijnck-Hughes and Wim Vanderbauwhede

Published in: DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. Although tools can be written to address such a separation of concerns, such tooling is often hand written and used to check hardware designs a posteriori. We have developed a dependent type-system and proof-of-concept modelling language to reason about the physical structure of hardware interfaces respective to user provided descriptions. Our type-system provides correct-by-construction guarantees that the interfaces on an IP Core will be well-typed if they adhere to a specified standard.
Cite as

Jan de Muijnck-Hughes and Wim Vanderbauwhede. A Typing Discipline for Hardware Interfaces (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 14:1-14:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{demuijnckhughes_et_al:DARTS.5.2.14,
  author =	{de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
  title =	{{A Typing Discipline for Hardware Interfaces}},
  pages =	{14:1--14:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{2},
  editor =	{de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.2.14},
  URN =		{urn:nbn:de:0030-drops-107919},
  doi =		{10.4230/DARTS.5.2.14},
  annote =	{Keywords: System-on-a-Chip, AXI, Dependent Types, Substructural Typing}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2019.6
A Typing Discipline for Hardware Interfaces

Authors: Jan de Muijnck-Hughes and Wim Vanderbauwhede

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. Although tools can be written to address such separation of concerns, the tooling is often hand written and used to check hardware designs a posteriori. We have developed a dependent type-system and proof-of-concept modelling language to reason about the physical structure of hardware interfaces using user provided descriptions. Our type-system provides correct-by-construction guarantees that the interfaces on an IP Core will be well-typed if they adhere to a specified standard.
Cite as

Jan de Muijnck-Hughes and Wim Vanderbauwhede. A Typing Discipline for Hardware Interfaces. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 6:1-6:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{demuijnckhughes_et_al:LIPIcs.ECOOP.2019.6,
  author =	{de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
  title =	{{A Typing Discipline for Hardware Interfaces}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{6:1--6:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.6},
  URN =		{urn:nbn:de:0030-drops-107983},
  doi =		{10.4230/LIPIcs.ECOOP.2019.6},
  annote =	{Keywords: System-on-a-Chip, AXI, Dependent Types, Substructural Typing}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact