Typing untyped \(\lambda\)-terms, or reducibility strikes again!
type: Item
instance of: scholarly article
title: Typing untyped \(\lambda\)-terms, or reducibility strikes again!
zbMATH Open document ID: 0930.03011
DOI: 10.1016/S0168-0072(97)00047-X
published in: Annals of Pure and Applied Logic
publication date: 2000-02-15T00:00:00Z
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 1308055
zbMATH Keywords: type assignment
zbMATH Keywords: lambda calculus
zbMATH Keywords: conjunctive types
zbMATH Keywords: normalizable terms
zbMATH Keywords: meta-theorems relating properties of \(\lambda\)-terms and their typability
zbMATH Keywords: reducibility
zbMATH Keywords: weak head-normal forms
zbMATH Keywords: realizability method
author: Jean Gallier
MaRDI profile type: Publication
cites work: A new type assignment for λ-terms
cites work: An extension of basic functionality theory for \(\lambda\)-calculus
cites work: Functional Characters of Solvable Terms
cites work: Q5691056
cites work: Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves
cites work: Q5625124
cites work: Q4281473
cites work: Church-Rosser theorem for typed functional systems
cites work: Q3997016
cites work: A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
cites work: Q3922646
cites work: Intensional interpretations of functionals of finite type I
cites work: Q4093416
full work available at URL: s0168-0072(97)00047-x
OpenAlex ID: W1520157111
description: scientific article; zbMATH DE number 1308055