@inproceedings{a0b826d1e7344b528db9f98b02882224,

title = "Dependently typed programming with finite sets",

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.",

keywords = "Agda, Bishop finiteness, Certified programming, Dependently typed programming, Finite sets, Kuratowski finiteness",

author = "Denis Firsov and Tarmo Uustalu",

year = "2015",

month = aug,

day = "30",

doi = "10.1145/2808098.2808102",

language = "English",

series = "WGP 2015 - Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, co-located with ICFP 2015",

publisher = "Association for Computing Machinery, Inc",

pages = "33--44",

editor = "Patrick Bahr and Sebastian Erdweg",

booktitle = "WGP 2015 - Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, co-located with ICFP 2015",

note = "11th ACM SIGPLAN Workshop on Generic Programming, WGP 2015 ; Conference date: 30-08-2015",

}