2023/06/13 by Gilles Dowek, Dowek, Gilles
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies
paper · doi:10.48550/arxiv.2306.07599
openalex publication_date 2023/06/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.