A discrimination algorithm inside \(\lambda -\beta\)-calculus

DOI10.1016/0304-3975(79)90014-8zbMath0405.03005OpenAlexW1983495063WikidataQ123239568 ScholiaQ123239568MaRDI QIDQ1257009

P. Peretti, Simonetta Ronchi della Rocca, Mariangiola Dezani-Ciancaglini

Publication date: 1979

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(79)90014-8

zbMATH Keywords

Normal FormDiscrimination AlgorithmLambda-Beta Calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (14)

Effective applicative structures ⋮ Monotone recursive types and recursive data representations in Cedille ⋮ Storage operators and directed lambda-calculus ⋮ Unnamed Item ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ Parametric \(\lambda \)-theories ⋮ Böhm’s Theorem for Resource Lambda Calculus through Taylor Expansion ⋮ Strong storage operators and data types ⋮ Unnamed Item ⋮ About systems of equations, X-separability, and left-invertibility in the \(\lambda\)-calculus ⋮ The discrimination theorem holds for combinatory weak reduction ⋮ An algebraic view of the Böhm-out technique ⋮ An analysis of Böhm's theorem ⋮ General recursive functions in a very simply interpretable typed \(\lambda\)-calculus

Cites Work

• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A discrimination algorithm inside \(\lambda -\beta\)-calculus