A few constructions on constructors

Conor McBride, Healfdene Goguen, James McKinna

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Citations (Scopus)

Abstract

We present four constructions for standard equipment which can be generated for every inductive datatype: case analysis, structural recursion, no confusion, acyclicity. Our constructions follow a two-level approach - they require less work than the standard techniques which inspired them [11,8]. Moreover, given a suitably heterogeneous notion of equality, they extend without difficulty to inductive families of datatypes. These constructions are vital components of the translation from dependently typed programs in pattern matching style [7] to the equivalent programs expressed in terms of induction principles [21] and as such play a crucial behind-the-scenes rôle in Epigram [25].

Original languageEnglish
Title of host publicationTypes for Proofs and Programs. TYPES 2004
PublisherSpringer
Pages186-200
Number of pages15
ISBN (Electronic)9783540314295
ISBN (Print)9783540314288
DOIs
Publication statusPublished - 2006
EventInternational Workshop on Types for Proofs and Programs 2004 - Jouy-en-Josas, France
Duration: 15 Dec 200418 Dec 2004

Publication series

NameLecture Notes in Computer Science
Volume3839
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Workshop on Types for Proofs and Programs 2004
Abbreviated titleTYPES 2004
CountryFrance
CityJouy-en-Josas
Period15/12/0418/12/04

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A few constructions on constructors'. Together they form a unique fingerprint.

Cite this