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)
Preview |
Text.
Filename: Wood_Atkey_LTLLA_2020_A_linear_algebra_approach_to_linear_metatheory.pdf
Final Published Version License: 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: https://orcid.org/0000-0002-4414-5047;-
-
Item type: Article ID code: 74151 Dates: DateEvent30 December 2021Published29 June 2020Published Online15 May 2020AcceptedSubjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 08 Oct 2020 12:31 Last modified: 06 Nov 2024 01:53 URI: https://strathprints.strath.ac.uk/id/eprint/74151