Strong normalization for typed terms with surjective pairing

DOI10.1305/ndjfl/1093636767zbMath0624.03043OpenAlexW1981838174MaRDI QIDQ1092042

A. S. Troelstra

Publication date: 1986

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1305/ndjfl/1093636767

zbMATH Keywords

strong normalizationsurjective pairingCartesian product typesintuitionistic finite-type arithmetictyped terms

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40)

Related Items

On the syntax of Martin-Löf's type theories, Simulating expansions without expansions, A linear logical framework, A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object, A confluent reduction for the λ-calculus with surjective pairing and terminal object