Towards a proof theory of rewriting: the simply typed 2 -calculus

Publisher： Elsevier

ISSN： 0304-3975

Source： Theoretical Computer Science, Vol.170, Iss.1, 1996-12, pp. : 407-444

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

Related content

A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions

By Coquand C.

LISP and Symbolic Computation, Vol. 15, Iss. 1, 2002-03 ,pp. : 57-90

Springer Publishing Company

Access to resources Recommend Favorite

A typed context calculus

By Hashimoto

Theoretical Computer Science, Vol. 266, Iss. 1, 2001-09 ,pp. : 249-272

Elsevier

Access to resources Recommend Favorite

Proof theory of higher-order equations: conservativity, normal forms and term rewriting

By Meinke K.

Journal of Computer and System Sciences, Vol. 67, Iss. 1, 2003-08 ,pp. : 127-173

Elsevier

Access to resources Recommend Favorite

Comparing models of the intensional typed -calculus

By Hoofman R.

Theoretical Computer Science, Vol. 166, Iss. 1, 1996-10 ,pp. : 83-99

Elsevier

Access to resources Recommend Favorite

Typed generic traversal with term rewriting strategies

By Lammel R.

Journal of Logic and Algebraic Programming, Vol. 54, Iss. 1, 2003-01 ,pp. : 1-64

Elsevier

Access to resources Recommend Favorite