A linear algebra approach to linear metatheory

Research output: Contribution to conferencePaper

2 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 languageEnglish
Number of pages8
Publication statusPublished - 29 Jun 2020
EventLinearity & Trends in Linear Logic and its Application 2020 - Online
Duration: 29 Jun 202030 Jun 2020
Conference number: 2
https://lipn.univ-paris13.fr/LinearityTLLA2020/

Conference

ConferenceLinearity & Trends in Linear Logic and its Application 2020
Abbreviated titleLinearity-TLLA
Period29/06/2030/06/20
Internet address

Keywords

  • linear algebra
  • renaming
  • variables

Fingerprint Dive into the research topics of 'A linear algebra approach to linear metatheory'. Together they form a unique fingerprint.

  • Cite this

    Wood, J., & Atkey, R. (2020). A linear algebra approach to linear metatheory. Paper presented at Linearity & Trends in Linear Logic and its Application 2020, .