@inproceedings{31503b5cc5654272bd89bc20cebf9ce1,

title = "A typed lambda calculus with categorical type constructors",

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.",

author = "Tatsuya Hagino",

note = "Publisher Copyright: {\textcopyright} 1987, Springer-Verlag.; International Conference on Category Theory and Computer Science, 1987 ; Conference date: 07-09-1987 Through 09-09-1987",

year = "1987",

doi = "10.1007/3-540-18508-9_24",

language = "English",

isbn = "9783540185086",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "140--157",

editor = "Pitt, {David H.} and Axel Poigne and Rydeheard, {David E.}",

booktitle = "Category Theory and Computer Science, Proceedings",

}