A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language

Publisher： Cambridge University Press

E-ISSN： 1943-5886|76|2|673-699

ISSN： 0022-4812

Source： The Journal of Symbolic Logic, Vol.76, Iss.2, 2011-06, pp. : 673-699

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

Analytic proof systems for λ-calculus: the elimination of transitivity, and why it matters

By Minari Pierluigi  

Archive for Mathematical Logic, Vol. 46, Iss. 5-6, 2007-07 ,pp. : 385-424

Springer Publishing Company

Access to resources Recommend Favorite

A proof-theoretic investigation of a logic of positions

By Baratella S.   Masini A.  

Annals of Pure and Applied Logic, Vol. 123, Iss. 1, 2003-10 ,pp. : 135-162

Elsevier

Access to resources Recommend Favorite

A proof of the cut-elimination theorem in simple type theory

By  

The Journal of Symbolic Logic, Vol. 38, Iss. 2, 1973-06 ,pp. : 215-226

Cambridge University Press

Access to resources Recommend Favorite

The λ-calculus is ω-incomplete

By  

The Journal of Symbolic Logic, Vol. 39, Iss. 2, 1974-06 ,pp. : 313-317

Cambridge University Press

Access to resources Recommend Favorite

A proof-theoretic study of the correspondence of classical logic and modal logic

By  

The Journal of Symbolic Logic, Vol. 68, Iss. 4, 2003-12 ,pp. : 1403-1414

Cambridge University Press

Access to resources Recommend Favorite