An upper bound for reduction sequences in the typed λ-calculus

Archive for Mathematical Logic 30 (5-6):405-408 (1991)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1007/bf01621476

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 100,290

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

Analyzing Godel's T Via Expanded Head Reduction Trees.Arnold Beckmann & Andreas Weiermann - 2000 - Mathematical Logic Quarterly 46 (4):517-536.
Exact Bounds for lengths of reductions in typed λ-calculus.Arnold Beckmann - 2001 - Journal of Symbolic Logic 66 (3):1277-1285.
Upper Bounds for Standardizations and an Application.Hongwei Xi - 1999 - Journal of Symbolic Logic 64 (1):291-303.
Continuous normalization for the lambda-calculus and Gödel’s T.Klaus Aehlig & Felix Joachimski - 2005 - Annals of Pure and Applied Logic 133 (1-3):39-71.
Choice sequences and reduction processes.R. Haberthür - 1978 - Archive for Mathematical Logic 19 (1):31-49.
A typed λ-calculus and Girard's model of ptykes.Peter Päppinghaus - 1985 - In G. Dorn & P. Weingarten (eds.), Foundations of Logic and Linguistics. Problems and Solutions. Plenum. pp. 245--279.
Herbrand complexity and the epsilon calculus with equality.Kenji Miyamoto & Georg Moser - 2023 - Archive for Mathematical Logic 63 (1):89-118.
The Weak Normalization of the Simply Typed λse-calculus.Ariel Arbiser, Fairouz Kamareddine & Alejandro Rios - 2007 - Logic Journal of the IGPL 15 (2):121-147.
A Mixed λ-calculus.Marie-Renée Fleury & Myriam Quatrini - 2007 - Studia Logica 87 (2-3):269-294.
Short proofs of normalization for the simply- typed λ-calculus, permutative conversions and Gödel's T.Felix Joachimski & Ralph Matthes - 2003 - Archive for Mathematical Logic 42 (1):59-87.

Analytics

Added to PP
2013-11-23

Downloads
64 (#327,104)

6 months
8 (#549,811)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Exact Bounds for lengths of reductions in typed λ-calculus.Arnold Beckmann - 2001 - Journal of Symbolic Logic 66 (3):1277-1285.
Elementary Proof of Strong Normalization for Atomic F.Fernando Ferreira & Gilda Ferreira - 2016 - Bulletin of the Section of Logic 45 (1):1-15.
A decidable theory of type assignment.William R. Stirton - 2013 - Archive for Mathematical Logic 52 (5-6):631-658.

View all 6 citations / Add more citations

References found in this work

Functionals defined by recursion.Luis Elpidio Sanchis - 1967 - Notre Dame Journal of Formal Logic 8 (3):161-174.
Ordinal analysis of terms of finite type.W. A. Howard - 1980 - Journal of Symbolic Logic 45 (3):493-504.

Add more references