The Undecidability of Typability in the Lambda-Pi-Calculus
Logic in Computer Science
2023-06-14 v1
Abstract
The set of pure terms which are typable in the -calculus in a given context is not recursive. So there is no general type inference algorithm for the programming language Elf and, in some cases, some type information has to be mentioned by the programmer.
Keywords
Cite
@article{arxiv.2306.07599,
title = {The Undecidability of Typability in the Lambda-Pi-Calculus},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2306.07599},
year = {2023}
}