Random Generators for Dependent Types

by: Peter Dybjer, Qiao Haiyan, Makoto Takeyama

Theoretical Aspects of Computing - ICTAC 2004 (2005), pp. 341-355.

View FullText article

SpringerLink

Reviews [Write a review of this article]

There are no reviews of this article

Find related articles from these CiteULike users

shimomura, msakai

Find related articles with these CiteULike tags

2005, dependenttype, dependent-types, testing, type-theory

Abstract

We show how to write surjective random generators for several different classes of inductively defined types in dependent type theory. We discuss both non-indexed (simple) types and indexed families of types. In particular we show how to use the relationship between indexed inductive definitions and logic programs: the indexed inductive definition of a type family corresponds to a logic program, and generating an object of a type in the family corresponds to solving a query for the logic program. As an example, we show how to write a surjective random generator for theorems in propositional logic by randomising the Prolog search algorithm.

@incollection{citeulike:2919442, abstract = {We show how to write surjective random generators for several different classes of inductively defined types in dependent type theory. We discuss both non-indexed (simple) types and indexed families of types. In particular we show how to use the relationship between indexed inductive definitions and logic programs: the indexed inductive definition of a type family corresponds to a logic program, and generating an object of a type in the family corresponds to solving a query for the logic program. As an example, we show how to write a surjective random generator for theorems in propositional logic by randomising the Prolog search algorithm.}, author = {Dybjer, Peter and Haiyan, Qiao and Takeyama, Makoto }, citeulike-article-id = {2919442}, journal = {Theoretical Aspects of Computing - ICTAC 2004}, keywords = {2005, dependenttype, testing}, pages = {341--355}, posted-at = {2008-06-23 18:22:09}, priority = {2}, title = {Random Generators for Dependent Types}, url = {http://www.springerlink.com/content/adarfqwjd01pgung }, year = {2005} }

RIS record

TY - CHAP ID - citeulike:2919442 L3 - citeulike-article-id:2919442 TI - Random Generators for Dependent Types JF - Theoretical Aspects of Computing - ICTAC 2004 SP - 341 EP - 355 N2 - We show how to write surjective random generators for several different classes of inductively defined types in dependent type theory. We discuss both non-indexed (simple) types and indexed families of types. In particular we show how to use the relationship between indexed inductive definitions and logic programs: the indexed inductive definition of a type family corresponds to a logic program, and generating an object of a type in the family corresponds to solving a query for the logic program. As an example, we show how to write a surjective random generator for theorems in propositional logic by randomising the Prolog search algorithm. KW - 2005 KW - dependenttype KW - testing AU - Dybjer, Peter AU - Haiyan, Qiao AU - Takeyama, Makoto PY - 2005/// UR - http://www.springerlink.com/content/adarfqwjd01pgung ER -

RIS BibTeX