Non-standard reductions and categorical models in typed lambda-calculus.


F. Barral
D. Chemouil
S. Soloviev


We consider the problem of incorporation of new computational rules in lambda calculus with inductive types and recursion. We consider the extensions of standard reduction systems by certain new reductions preserving strong normalization and Church-Rosser property with possible applications to proof assistants and computer algebra systems.






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).