Computational Adequacy for Substructural Lambda Calculi - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2020

Computational Adequacy for Substructural Lambda Calculi

Résumé

Substructural type systems, such as affine (and linear) type systems, are type systems which impose restrictions on copying (and discarding) of variables, and they have found many applications in computer science, including quantum programming. We describe one linear and one affine type systems and we formulate abstract categorical models for both of them which are sound and computationally adequate. We also show, under basic assumptions, that interpreting lambda abstractions via a monoidal closed structure (a popular method for linear type systems) necessarily leads to degenerate and inadequate models for call-by-value affine type systems, so we avoid doing this in our categorical treatment, where a solution to this problem is clearly identified. Our categorical models are more general than linear/non-linear models used to study linear logic and we present a homogeneous categorical account of both linear and affine type systems in a call-by-value setting. We also give examples with many concrete models, including classical and quantum ones.

Dates et versions

hal-03018433 , version 1 (22-11-2020)

Identifiants

Citer

Vladimir Zamdzhiev. Computational Adequacy for Substructural Lambda Calculi. Applied Category Theory 2020, Jul 2020, Virtual, United States. ⟨10.4204/EPTCS.333.22⟩. ⟨hal-03018433⟩
27 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More