A linear algebra approach to linear metatheory

James Wood; Robert Atkey

doi:10.4204/EPTCS.353.10

A linear algebra approach to linear metatheory

James Wood, Robert Atkey

Research output: Contribution to journal › Conference Contribution › peer-review

4 Citations (Scopus)

37 Downloads (Pure)

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.

Original language	English
Pages (from-to)	195-212
Number of pages	8
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	354
Issue number	2021
Early online date	29 Jun 2020
DOIs	https://doi.org/10.4204/EPTCS.353.10
Publication status	Published - 30 Dec 2021
Event	Linearity & Trends in Linear Logic and its Application 2020 - Online Duration: 29 Jun 2020 → 30 Jun 2020 Conference number: 2 https://lipn.univ-paris13.fr/LinearityTLLA2020/

Keywords

linear algebra
renaming
variables

Access to Document

10.4204/EPTCS.353.10Licence: CC BY 4.0

Wood-Atkey-LTLLA-2020-A-linear-algebra-approach-to-linear-metatheoryFinal published version, 177 KBLicence: CC BY 4.0

Cite this

@article{8930aa411b50487f96402b16cb21ca00,

title = "A linear algebra approach to linear metatheory",

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.",

keywords = "linear algebra, renaming, variables",

author = "James Wood and Robert Atkey",

year = "2021",

month = dec,

day = "30",

doi = "10.4204/EPTCS.353.10",

language = "English",

volume = "354",

pages = "195--212",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

publisher = "Open Publishing Association",

number = "2021",

note = "Linearity & Trends in Linear Logic and its Application 2020, Linearity-TLLA ; Conference date: 29-06-2020 Through 30-06-2020",

url = "https://lipn.univ-paris13.fr/LinearityTLLA2020/",

}

TY - JOUR

T1 - A linear algebra approach to linear metatheory

AU - Wood, James

AU - Atkey, Robert

N1 - Conference code: 2

PY - 2021/12/30

Y1 - 2021/12/30

N2 - 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.

AB - 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.

KW - linear algebra

KW - renaming

KW - variables

U2 - 10.4204/EPTCS.353.10

DO - 10.4204/EPTCS.353.10

M3 - Conference Contribution

SN - 2075-2180

VL - 354

SP - 195

EP - 212

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

IS - 2021

T2 - Linearity & Trends in Linear Logic and its Application 2020

Y2 - 29 June 2020 through 30 June 2020

ER -

A linear algebra approach to linear metatheory

Abstract

Keywords

Access to Document

Fingerprint

Cite this