2026-07-24T05:11:47Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16774 2024-03-06T10:58:14Z ddc:004 open_access

Principal Types as Lambda Nets Di Gianantonio, Pietro Lenisa, Marina Lambda calculus Principal types Linear logic Lambda nets Normalization Cut elimination We show that there are connections between principal type schemata, cut-free λ-nets, and normal forms of the λ-calculus, and hence there are correspondences between the normalisation algorithms of the above structures, i.e. unification of principal types, cut-elimination of λ-nets, and normalisation of λ-terms. Once the above correspondences have been established, properties of the typing system, such as typability, subject reduction, and inhabitation, can be derived from properties of λ-nets, and vice-versa. We illustrate the above pattern on a specific type assignment system, we study principal types for this system, and we show that they correspond to λ-nets with a non-standard notion of cut-elimination. Properties of the type system are then derived from results on λ-nets. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pietro Di Gianantonio and Marina Lenisa 2022 Is Part Of LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2021.5 urn:nbn:de:0030-drops-167744 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.5 eng https://creativecommons.org/licenses/by/4.0/legalcode