Proof-term synthesis on dependent-type systems via explicit substitutions

Author： Munoz

Publisher： Elsevier

ISSN： 0304-3975

Source： Theoretical Computer Science, Vol.266, Iss.1, 2001-09, pp. : 407-440

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 -calculus with explicit substitutions

By Ferrari G.-L. Montanari U. Quaglia P.

Theoretical Computer Science, Vol. 168, Iss. 1, 1996-11 ,pp. : 53-103

Elsevier

Access to resources Recommend Favorite

Explicit substitutions for pi-congruences

By Quaglia P.

Theoretical Computer Science, Vol. 269, Iss. 1, 2001-10 ,pp. : 83-134

Elsevier

Access to resources Recommend Favorite

Confluence of extensional and non-extensional -calculi with explicit substitutions

By Kesner D.

Theoretical Computer Science, Vol. 238, Iss. 1, 2000-05 ,pp. : 183-220

Elsevier

Access to resources Recommend Favorite

Unique normal form property of compatible term rewriting systems: a new proof of Chew's theorem

By Mano K. Ogawa M.

Theoretical Computer Science, Vol. 258, Iss. 1, 2001-05 ,pp. : 169-208

Elsevier

Access to resources Recommend Favorite