Decidability and confluence of \(\beta\eta\text{top}_ \leqslant\) reduction in \({\mathbb{F}}_ \leqslant\)

DOI10.1006/inco.1994.1014zbMath0815.03006OpenAlexW2795046794MaRDI QIDQ1322474

Giorgio Ghelli, Pierre-Louis Curien

Publication date: 9 June 1994

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

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

zbMATH Keywords

reductiondecidabilitylambda calculussubtypingSystem Fbounded quantificationequality judgementsexplicit coercions

Mathematics Subject Classification ID

Theory of programming languages (68N15) Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Related Items

Termination of system \(F\)-bounded: A complete proof, Divergence of \(F_{\leq}\) type checking, Basic theory of \(F\)-bounded quantification.