Loading...
Please wait, while we are loading the content...
Similar Documents
Dependently typed programming with finite sets
| Content Provider | ACM Digital Library |
|---|---|
| Author | Uustalu, Tarmo Firsov, Denis |
| 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. . |
| Starting Page | 33 |
| Ending Page | 44 |
| Page Count | 12 |
| File Format | |
| ISBN | 9781450338103 |
| DOI | 10.1145/2808098.2808102 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2015-08-30 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Finite sets Dependently typed programming Bishop finiteness Agda Kuratowski finiteness Certified programming |
| Content Type | Text |
| Resource Type | Article |
