Indexed containers. (2015)
- Record Type:
- Journal Article
- Title:
- Indexed containers. (2015)
- Main Title:
- Indexed containers
- Authors:
- ALTENKIRCH, THORSTEN
GHANI, NEIL
HANCOCK, PETER
MCBRIDE, CONOR
MORRIS, PETER - Abstract:
- Abstract: We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide normal forms for strictly positive families in much the same way that containers provide normal forms for strictly positive types. Interestingly, this step from containers to indexed containers is achieved without having to extend the core type theory. Most of the construction presented here has been formalized using the Agda system.
- Is Part Of:
- Journal of functional programming. Volume 25(2015)
- Journal:
- Journal of functional programming
- Issue:
- Volume 25(2015)
- Issue Display:
- Volume 25, Issue 2015 (2015)
- Year:
- 2015
- Volume:
- 25
- Issue:
- 2015
- Issue Sort Value:
- 2015-0025-2015-0000
- Page Start:
- Page End:
- Publication Date:
- 2015
- Subjects:
- Functional programming (Computer science) -- Periodicals
- Journal URLs:
- http://journals.cambridge.org/action/displayJournal?jid=JFP ↗
http://firstsearch.oclc.org ↗ - DOI:
- 10.1017/S095679681500009X ↗
- Languages:
- English
- ISSNs:
- 0956-7968
- Deposit Type:
- Legaldeposit
- View Content:
- Available online (eLD content is only available in our Reading Rooms) ↗
- Physical Locations:
- British Library STI - ELD Digital store
- Ingest File:
- 4776.xml