License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.7.2.10
URN: urn:nbn:de:0030-drops-140342
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14034/
Go back to Dagstuhl Artifacts Series

Brady, Edwin

Idris 2: Quantitative Type Theory in Practice (Artifact)

pdf-format:
DARTS-7-2-10.pdf (0.5 MB)

Abstract

Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution.
Idris 2 is a new version of Idris, implemented in itself, and based on Quantitative Type Theory. The paper introduces Idris 2 and describes how QTT has influenced its design, as well as giving several examples of how to use QTT in practice. The artifact, correspondingly, provides an implementation of Idris 2, running on a virtual machine, along with runnable examples from the paper. This document explains how to install the artifact, how to run the examples, and suggests some small ways to experiment with and modify the examples.

BibTeX - Entry

@Article{brady:DARTS.7.2.10,
  author =	{Brady, Edwin},
  title =	{{Idris 2: Quantitative Type Theory in Practice (Artifact)}},
  pages =	{10:1--10:7},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Brady, Edwin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14034},
  URN =		{urn:nbn:de:0030-drops-140342},
  doi =		{10.4230/DARTS.7.2.10},
  annote =	{Keywords: Dependent types, linear types, concurrency}
}

Keywords: Dependent types, linear types, concurrency
Collection: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)
Related Scholarly Article: https://doi.org/10.4230/LIPIcs.ECOOP.2021.9
Issue Date: 2021
Date of publication: 06.07.2021

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