2026/07/18 by Ana Jorge Almeida, Sandra Alves, Mário Florido
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Formal Methods in Verification
paper · pdf · doi:10.4204/eptcs.449.2
Term expansion was originally introduced in 2004 as a way to relate terms typed in an intersection type system with linear terms. Recently, new applications of term expansion include the relation of lambda-terms with terms typed in other substructural type systems, such as the relevant and the ordered type systems, and the use of quantitative types to relate the strongly normalising lambda-terms with weak linear terms that share the same normal form. Here we define a new term expansion for a calculus with explicit substitutions, using it to relate a lambda-calculus with explicit substitutions to Boudol's resource aware lambda-calculus with multiplicities, where function arguments have a possibly limited availability.