A linear algebra approach to linear metatheory

Wood, James and Atkey, Robert (2021) A linear algebra approach to linear metatheory. Electronic Proceedings in Theoretical Computer Science, EPTCS, 354 (2021). pp. 195-212. ISSN 2075-2180 (https://doi.org/10.4204/EPTCS.353.10)

[thumbnail of Wood-Atkey-LTLLA-2020-A-linear-algebra-approach-to-linear-metatheory]
Preview
 Text. Filename: Wood_Atkey_LTLLA_2020_A_linear_algebra_approach_to_linear_metatheory.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (181kB)| Preview

Abstract

Linear typed λ-calculi are more delicate than their simply typed siblings when it comes to metatheoretic results like preservation of typing under renaming and substitution. Tracking the usage of variables in contexts places more constraints on how variables may be renamed or substituted. We present a methodology based on linear algebra over semirings, extending McBride's kits and traversals approach for the metatheory of syntax with binding to linear usage-annotated terms. Our approach is readily formalisable, and we have done so in Agda.

ORCID iDs

Wood, James and Atkey, Robert ORCID logoORCID: https://orcid.org/0000-0002-4414-5047;
CORE (COnnecting REpositories)