Dependently typed programming with finite sets

Denis Firsov, Tarmo Uustalu

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Citations (Scopus)

Abstract

Definitions of many mathematical structures used in computer science are parametrized by finite sets. To work with such structures in proof assistants, we need to be able to explain what a finite set is. In constructive mathematics, a widely used definition is listability: a set is considered to be finite, if its elements can be listed completely. In this paper, we formalize different variations of this definition in the Agda programming language. We develop a toolbox for boilerplate-free programming with finite sets that arise as subsets of some base set with decidable equality. Among other things we implement combinators for defining functions from finite sets and a prover for quantified formulas over decidable properties on finite sets.

Original languageEnglish
Title of host publicationWGP 2015 - Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, co-located with ICFP 2015
EditorsPatrick Bahr, Sebastian Erdweg
PublisherAssociation for Computing Machinery, Inc
Pages33-44
Number of pages12
ISBN (Electronic)9781450338103
DOIs
Publication statusPublished - 30 Aug 2015
Event11th ACM SIGPLAN Workshop on Generic Programming, WGP 2015 - Vancouver, Canada
Duration: 30 Aug 2015 → …

Publication series

NameWGP 2015 - Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, co-located with ICFP 2015

Conference

Conference11th ACM SIGPLAN Workshop on Generic Programming, WGP 2015
Country/TerritoryCanada
CityVancouver
Period30/08/15 → …

Other keywords

  • Agda
  • Bishop finiteness
  • Certified programming
  • Dependently typed programming
  • Finite sets
  • Kuratowski finiteness

Fingerprint

Dive into the research topics of 'Dependently typed programming with finite sets'. Together they form a unique fingerprint.

Cite this