Decidability and confluence of \(\beta\eta\text{top}_ \leqslant\) reduction in \({\mathbb{F}}_ \leqslant\)
From MaRDI portal
Publication:1322474
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
reductiondecidabilitylambda calculussubtypingSystem Fbounded quantificationequality judgementsexplicit coercions
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.
