A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond

DOI10.1006/INCO.1995.1132zbMath0833.68075OpenAlexW2078295617MaRDI QIDQ1899911

D. F. Otth, David Allen McAllester, Jakov Kučan

Publication date: 10 October 1995

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1995.1132

zbMATH Keywords

strong normalizationevaluation technique

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55)

Related Items (6)

Strong normalization for non-structural subtyping via saturated sets ⋮ Termination of system \(F\)-bounded: A complete proof ⋮ Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves ⋮ Hybrid interactive theorem proving using nuprl and HOL ⋮ Typing untyped \(\lambda\)-terms, or reducibility strikes again! ⋮ Basic theory of \(F\)-bounded quantification.

This page was built for publication: A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond