A decidable theory of type assignment (Q365669): Difference between revisions
From MaRDI portal
Changed an Item |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 01:04, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A decidable theory of type assignment |
scientific article |
Statements
A decidable theory of type assignment (English)
0 references
9 September 2013
0 references
This is an important, interesting and well written paper. It's contents are well described in the author's abstract which I quote: This article investigates a theory of type assignment (assigning types to lambda terms) called ETA which is intermediate in strength between the simple theory of type assignment and strong polymorphic theories like Girard's F [\textit{J.-Y. Girard} et al., Proofs and types. Cambridge etc.: Univ. Press (1989; Zbl 0671.68002)]. It is like the simple type theory and unlike F in that the typability and type-checking problems are solvable with respect to ETA. This is proved in the article along with three other main results: (1) all primitive recusive functionals of finite type are representable in ETA; (2) every term typable in ETA has a unique normal form; (3) there is a function defined by \(\epsilon_0\)-recursion which takes every typable term to a natural number which is an upper bound to the lengths of all \(\beta \eta\)-reduction sequences starting with that term.
0 references
type assignment
0 references
lambda calculus
0 references
primitive recursive functionals
0 references
type reconstruction
0 references
typability
0 references
type checking
0 references
reduction sequences
0 references