Some lambda calculi with categorical sums and products. Dougherty, D. J.\ 1993. Paper abstract bibtex We consider the simply typed $łambda$-calculus with primitive recursion operators and types corresponding to categorical products and coproducts. The standard equations corresponding to extensionality and to surjectivity of pairing and its dual are oriented as expansion rules. Strong normalization and ground (base-type) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latter case, fixed-point constructors may be added while retaining confluence.
@conference{ c_rta93,
author = {Daniel J.\ Dougherty},
title = {Some lambda calculi with categorical sums and
products},
pages = {137--151},
isbn = {3-540-56868-9},
editor = {Claude Kirchner},
booktitle = {Proc.\ 5th International Conference on
Rewriting Techniques and Applications ({RTA})},
series = {Lecture Notes in Computer Science},
volume = {690},
publisher = {Springer-Verlag},
address = {Berlin},
year = {1993},
abstract = { We consider the simply typed
$łambda$-calculus with primitive recursion
operators and types corresponding to
categorical products and coproducts. The
standard equations corresponding to
extensionality and to surjectivity of pairing
and its dual are oriented as expansion
rules. Strong normalization and ground
(base-type) confluence is proved for the full
calculus; full confluence is proved for the
calculus omitting the rule for strong sums. In
the latter case, fixed-point constructors may
be added while retaining confluence. },
url = {rta93.pdf}
}
Downloads: 0
{"_id":{"_str":"51f6934359ced8df44000e5e"},"__v":1,"authorIDs":[],"author_short":["Dougherty, D.<nbsp>J.\\"],"bibbaseid":"dougherty-somelambdacalculiwithcategoricalsumsandproducts-1993","bibdata":{"html":"<div class=\"bibbase_paper\"> \n\n\n<span class=\"bibbase_paper_titleauthoryear\">\n\t<span class=\"bibbase_paper_title\"><a name=\"c_rta93\"> </a>Some lambda calculi with categorical sums and products.</span>\n\t<span class=\"bibbase_paper_author\">\nDougherty, D. J.\\</span>\n\t<!-- <span class=\"bibbase_paper_year\">1993</span>. -->\n</span>\n\n\n\n 1993.\n\n\n\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content\">\n \n \n <!-- <i -->\n <!-- onclick=\"javascript:log_download('dougherty-somelambdacalculiwithcategoricalsumsandproducts-1993', 'http://web.cs.wpi.edu/~dd/publications/rta93.pdf')\">DEBUG -->\n <!-- </i> -->\n\n <a href=\"http://web.cs.wpi.edu/~dd/publications/rta93.pdf\"\n onclick=\"javascript:log_download('dougherty-somelambdacalculiwithcategoricalsumsandproducts-1993', 'http://web.cs.wpi.edu/~dd/publications/rta93.pdf')\">\n <img src=\"http://bibbase.org/img/filetypes/pdf.png\"\n\t alt=\"Some lambda calculi with categorical sums and products [.pdf]\" \n\t class=\"bibbase_icon\"\n\t style=\"width: 24px; height: 24px; border: 0px; vertical-align: text-top\" ><span class=\"bibbase_icon_text\">Paper</span></a> \n \n \n \n <a href=\"javascript:showBib('c_rta93')\"\n class=\"bibbase link\">\n <!-- <img src=\"http://bibbase.org/img/filetypes/bib.png\" -->\n\t<!-- alt=\"Some lambda calculi with categorical sums and products [bib]\" -->\n\t<!-- class=\"bibbase_icon\" -->\n\t<!-- style=\"width: 24px; height: 24px; border: 0px; vertical-align: text-top\"><span class=\"bibbase_icon_text\">Bibtex</span> -->\n BibTeX\n <i class=\"fa fa-caret-down\"></i></a>\n \n \n \n <a class=\"bibbase_abstract_link bibbase link\"\n href=\"javascript:showAbstract('c_rta93')\">\n Abstract\n <i class=\"fa fa-caret-down\"></i></a>\n \n \n \n\n \n \n \n</span>\n\n<div class=\"well well-small bibbase\" id=\"bib_c_rta93\"\n style=\"display:none\">\n <pre>@conference{ c_rta93,\n author = {Daniel J.\\ Dougherty},\n title = {Some lambda calculi with categorical sums and\n products},\n pages = {137--151},\n isbn = {3-540-56868-9},\n editor = {Claude Kirchner},\n booktitle = {Proc.\\ 5th International Conference on\n Rewriting Techniques and Applications ({RTA})},\n series = {Lecture Notes in Computer Science},\n volume = {690},\n publisher = {Springer-Verlag},\n address = {Berlin},\n year = {1993},\n abstract = { We consider the simply typed\n $łambda$-calculus with primitive recursion\n operators and types corresponding to\n categorical products and coproducts. The\n standard equations corresponding to\n extensionality and to surjectivity of pairing\n and its dual are oriented as expansion\n rules. Strong normalization and ground\n (base-type) confluence is proved for the full\n calculus; full confluence is proved for the\n calculus omitting the rule for strong sums. In\n the latter case, fixed-point constructors may\n be added while retaining confluence. },\n url = {rta93.pdf}\n}</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" id=\"abstract_c_rta93\"\n style=\"display:none\">\n We consider the simply typed $łambda$-calculus with primitive recursion operators and types corresponding to categorical products and coproducts. The standard equations corresponding to extensionality and to surjectivity of pairing and its dual are oriented as expansion rules. Strong normalization and ground (base-type) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latter case, fixed-point constructors may be added while retaining confluence.\n</div>\n\n\n</div>\n","downloads":0,"bibbaseid":"dougherty-somelambdacalculiwithcategoricalsumsandproducts-1993","urls":{"Paper":"http://web.cs.wpi.edu/~dd/publications/rta93.pdf"},"role":"author","abstract":"We consider the simply typed $łambda$-calculus with primitive recursion operators and types corresponding to categorical products and coproducts. The standard equations corresponding to extensionality and to surjectivity of pairing and its dual are oriented as expansion rules. Strong normalization and ground (base-type) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latter case, fixed-point constructors may be added while retaining confluence.","address":"Berlin","author":["Dougherty, Daniel J.\\"],"author_short":["Dougherty, D.<nbsp>J.\\"],"bibtex":"@conference{ c_rta93,\n author = {Daniel J.\\ Dougherty},\n title = {Some lambda calculi with categorical sums and\n products},\n pages = {137--151},\n isbn = {3-540-56868-9},\n editor = {Claude Kirchner},\n booktitle = {Proc.\\ 5th International Conference on\n Rewriting Techniques and Applications ({RTA})},\n series = {Lecture Notes in Computer Science},\n volume = {690},\n publisher = {Springer-Verlag},\n address = {Berlin},\n year = {1993},\n abstract = { We consider the simply typed\n $łambda$-calculus with primitive recursion\n operators and types corresponding to\n categorical products and coproducts. The\n standard equations corresponding to\n extensionality and to surjectivity of pairing\n and its dual are oriented as expansion\n rules. Strong normalization and ground\n (base-type) confluence is proved for the full\n calculus; full confluence is proved for the\n calculus omitting the rule for strong sums. In\n the latter case, fixed-point constructors may\n be added while retaining confluence. },\n url = {rta93.pdf}\n}","bibtype":"conference","booktitle":"Proc.\\ 5th International Conference on Rewriting Techniques and Applications (RTA)","editor":["Kirchner, Claude"],"editor_short":["Kirchner, C."],"id":"c_rta93","isbn":"3-540-56868-9","key":"c_rta93","pages":"137--151","publisher":"Springer-Verlag","series":"Lecture Notes in Computer Science","title":"Some lambda calculi with categorical sums and products","type":"conference","url":"rta93.pdf","volume":"690","year":"1993"},"bibtype":"conference","biburl":"http://web.cs.wpi.edu/~dd/publications/index.bib","downloads":0,"search_terms":["lambda","calculi","categorical","sums","products","dougherty"],"title":"Some lambda calculi with categorical sums and products","year":1993,"dataSources":["HB5RrPb3Y5aikRoLH"]}