Non-standard reductions and categorical models in typed lambda-calculus.
Article Sidebar
Опубликован:
30.11.2005
Main Article Content
Аннотация
Рассматривается проблема добавления новых правил вычисления к лямбда-исчислению с индуктивными типами и рекурсией. Рассматриваются расширения стандартных систем редукции при помощи новых редукций, сохраняющих строгую нормализацию и свойство Черча-Россера. Эти расширения имеют возможные приложения в областях компьютерных помощников поиска доказательств и систем компьютерной алгебры.
Скачивания
Данные скачивания пока не доступны.
Article Details
Как цитировать
Баррал Ф., Шемуи Д., Соловьев С. Non-standard reductions and categorical models in typed lambda-calculus. // Логические исследования / Logical Investigations. 2005. Т. 12. C. 300-315.
Выпуск
Раздел
Статьи
Литература
Akama Y. On Mints’ reductions for ccc-calculus // Lecture Notes in Computer Science. Vol. 664. P.l-12 (1993).
Baader F. and Nipkow T. Term rewriting and all that. Cambridge University Press, N. Y., 1998.
Bachmair L. and Dershowitz N. Commutation, transformation and termination // Lecture Notes in Computer Science. Vol. 230. P. 5-20 (1986).
Barendregt H. and Barendsen E. Autarkic computations in formal proofs // J. Autom. Reasoning. Vol. 28(3). P. 321-336 (2002).
Chemouil D. "Types inductifs, isomorphismes et recriture extensionnelle". Ph.d. thesis. Universite Toulouse 3 (2004).
Chemouil D. and Soloviev S. Remarks on isomorphisms of Simple Inductive Types // H. Geuvers, F. Kamareddine, eds. Electronic Notes in Theoretical Computer Science. Vol. 85. Elsevier (2003).
Di Cosmo R. On the power of simple diagrams // Harald Ganzinger, ed. Proceedings of the 7-th international Conference on Rewriting Techniques and Applications (RTA- 96). Lecture Notes in Computer Science. Vol. 1103. P. 200-214, Springer (1996).
Gezer A. "Relative termination". Ph.D. thesis. University of Passau, Germany (1990).
Soloviev S. and Chemouil D. Some algebraic structures in lambda-calculus with inductive types // Stefano Berardi, Mario Coppo and Ferruccio Damiani, eds. Proc. Types’03. Lecture Notes in Computer Science. Vol. 3085, Springer (2004).
Walukiewicz-Chrzaszcz D. Termination of rewriting in the calculus of constructions // J. of Functional Programming. Vol. 13(2). P. 339-414 (2003).
Baader F. and Nipkow T. Term rewriting and all that. Cambridge University Press, N. Y., 1998.
Bachmair L. and Dershowitz N. Commutation, transformation and termination // Lecture Notes in Computer Science. Vol. 230. P. 5-20 (1986).
Barendregt H. and Barendsen E. Autarkic computations in formal proofs // J. Autom. Reasoning. Vol. 28(3). P. 321-336 (2002).
Chemouil D. "Types inductifs, isomorphismes et recriture extensionnelle". Ph.d. thesis. Universite Toulouse 3 (2004).
Chemouil D. and Soloviev S. Remarks on isomorphisms of Simple Inductive Types // H. Geuvers, F. Kamareddine, eds. Electronic Notes in Theoretical Computer Science. Vol. 85. Elsevier (2003).
Di Cosmo R. On the power of simple diagrams // Harald Ganzinger, ed. Proceedings of the 7-th international Conference on Rewriting Techniques and Applications (RTA- 96). Lecture Notes in Computer Science. Vol. 1103. P. 200-214, Springer (1996).
Gezer A. "Relative termination". Ph.D. thesis. University of Passau, Germany (1990).
Soloviev S. and Chemouil D. Some algebraic structures in lambda-calculus with inductive types // Stefano Berardi, Mario Coppo and Ferruccio Damiani, eds. Proc. Types’03. Lecture Notes in Computer Science. Vol. 3085, Springer (2004).
Walukiewicz-Chrzaszcz D. Termination of rewriting in the calculus of constructions // J. of Functional Programming. Vol. 13(2). P. 339-414 (2003).