Typing and computational properties of lambda expressions (Q1819575): Difference between revisions
From MaRDI portal
Changed an Item |
Changed an Item |
||
| Property / describes a project that uses | |||
| Property / describes a project that uses: Automath / rank | |||
Normal rank | |||
Revision as of 13:49, 28 February 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Typing and computational properties of lambda expressions |
scientific article |
Statements
Typing and computational properties of lambda expressions (English)
0 references
1986
0 references
This paper integrates and generalizes known techniques and results (in particular, by the works of Girard and Coppo, Dezani \& Veneri) relating typing to convergence properties (such as normalizability) in the lambda calculus. It does so by considering types as semantical properties of \(\lambda\)-expressions in second-order models over \(\lambda\)-expressions. Working in the semantic discipline permits a richer notion of type and, therefore, more general results.
0 references
lambda expressions
0 references
typing
0 references
convergence
0 references
normalizability
0 references
lambda calculus
0 references
semantical properties
0 references
second-order models
0 references
