27 citations · 53 across the 14 of their papers we have counts for
Showing 2020Show all
2 papers · 1 filter
cs.PL2020★ 8 cited
A Linear Algebra Approach to Linear Metatheory
James Wood, Robert Atkey
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. Trac…
cs.PL2020
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
Guillaume Allais, Robert Atkey, James Chapman +2
Almost every programming language's syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of -equivalence, capture-avoiding…