Proofs of the normalization and Church-Rosser theorems for the typed $\lambda$-calculus

Notre Dame Journal of Formal Logic 19 (3):445-451 (1978)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1305/ndjfl/1093888405

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

The Church-Rosser theorem for the typed $\lambda$-calculus with surjective pairing.Garrel Pottinger - 1981 - Notre Dame Journal of Formal Logic 22 (3):264-268.
Remarks on the church-Rosser property.E. G. K. López-Escobar - 1990 - Journal of Symbolic Logic 55 (1):106-112.
On proof terms and embeddings of classical substructural logics.Ken-Etsu Fujita - 1998 - Studia Logica 61 (2):199-221.
Lambda Calculi: A Guide for the Perplexed.Chris Hankin - 1994 - Oxford University Press.
Alonzo church:his life, his work and some of his miracles.Maía Manzano - 1997 - History and Philosophy of Logic 18 (4):211-232.
Identity of proofs based on normalization and generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.
Lectures on the Curry-Howard isomorphism.Morten Heine Sørensen - 2007 - Boston: Elsevier. Edited by Paweł Urzyczyn.
An informal exposition of proofs of gödel's theorems and church's theorem.Barkley Rosser - 1939 - Journal of Symbolic Logic 4 (2):53-60.
Proofs are Programs: 19th Century Logic and 21st Century Computing.Philip Wadler - manuscript
A short introduction to intuitionistic logic.G. E. Mint︠s︡ - 2000 - New York: Kluwer Academic / Plenum Publishers.
Strong Normalizability of Typed Lambda-Calculi for Substructural Logics.Motohiko Mouri & Norihiro Kamide - 2008 - Logica Universalis 2 (2):189-207.
A Simplified Proof of the Church–Rosser Theorem.Yuichi Komori, Naosuke Matsuda & Fumika Yamakawa - 2014 - Studia Logica 102 (1):175-183.
Arithmetic based on the church numerals in illative combinatory logic.M. W. Bunder - 1988 - Studia Logica 47 (2):129 - 143.

Analytics

Added to PP
2010-08-24

Downloads
11 (#1,110,001)

6 months
6 (#504,917)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

No references found.

Add more references