Dependently typed programming with finite sets | Zendy

Denis Firsov | Zendy; Tarmo Uustalu | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Dependently typed programming with finite sets

Author(s) -

Denis Firsov,

Tarmo Uustalu

Publication year - 2015

Publication title -

citeseer x (the pennsylvania state university)

Language(s) - English

Resource type - Conference proceedings

DOI - 10.1145/2808098.2808102

Subject(s) - combinatory logic , computer science , decidability , programming language , gas meter prover , finite set , constructive , set (abstract data type) , theoretical computer science , base (topology) , mathematics , mathematical proof , mathematical analysis , geometry , process (computing)

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research