A typed lambda calculus with categorical type constructors

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

67 Citations (Scopus)

Abstract

A typed lambda calculus with categorical type constructors is introduced. It has a uniform category theoretic mechanism to declare new types. Its type structure includes categorical objects like products and coproducts as well as recursive types like natural numbers and lists. It also allows duals of recursive types, i.e. lazy types, like infinite lists. It has generalized iterators for recursive types and duals of iterators for lazy types. We will give reduction rules for this simply typed lambda calculus and show that they are strongly normalizing even though it has infinite things like infinite lists.

Original languageEnglish
Title of host publicationCategory Theory and Computer Science, Proceedings
EditorsDavid H. Pitt, Axel Poigne, David E. Rydeheard
PublisherSpringer Verlag
Pages140-157
Number of pages18
ISBN (Print)9783540185086
DOIs
Publication statusPublished - 1987
Externally publishedYes
EventInternational Conference on Category Theory and Computer Science, 1987 - Edinburgh, United Kingdom
Duration: 1987 Sep 71987 Sep 9

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume283 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Category Theory and Computer Science, 1987
CountryUnited Kingdom
CityEdinburgh
Period87/9/787/9/9

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A typed lambda calculus with categorical type constructors'. Together they form a unique fingerprint.

Cite this