2021/02/15 by Pierre Vial, Vial, Pierre
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #cs-LO #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2102.07515
openalex publication_date 2021/02/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We introduce a new representation of non-idempotent intersection types, using sequences (families indexed with natural numbers) instead of lists or multisets. This allows scaling up intersection type theory to the infinitary λ-calculus. We thus characterize hereditary head normalization, which gives a positive answer to a question known as Klop's Problem. On our way, we use non-idempotent intersection to retrieve some well-known results on infinitary terms.