2026-07-24T01:45:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20337 2024-07-05T06:20:34Z ddc:004 open_access

Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions Dudenhefner, Andrej Pautasso, Daniele lambda-calculus simple types intersection types strong normalization mechanization perpetual reductions We provide a new, purely syntactical proof of strong normalization for the simply typed λ-calculus. The result relies on a novel proof of the equivalence between typability in the simple type system and typability in the uniform intersection type system (a restriction of the non-idempotent intersection type system). For formal verification, the equivalence is mechanized using the Coq proof assistant. In the present work, strong normalization of a given simply typed term M is shown in four steps. First, M is reduced to a normal form N via a suitable reduction strategy with a decreasing measure. Second, a uniform intersection type for the normal form N is inferred. Third, a uniform intersection type for M is constructed iteratively via subject expansion. Fourth, strong normalization of M is shown by induction on the size of the type derivation. A supplementary contribution is a family of perpetual reduction strategies, i.e. strategies which preserve infinite reduction paths. This family allows for subject expansion in the intersection type systems of interest, and contains a reduction strategy with a decreasing measure in the simple type system. A notable member of this family is Barendregt’s F_∞ reduction strategy. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrej Dudenhefner and Daniele Pautasso 2024 Is Part Of LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2024.8 urn:nbn:de:0030-drops-203371 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.8 eng https://creativecommons.org/licenses/by/4.0/legalcode