So I've been mechanizing some simple linear lambda calculus stuff.

The basic framework is

$$ \frac{}{x \colon t \vdash x\colon t} $$

$$ \frac{\Gamma \vdash e \colon t \rightarrow t' \quad \Delta \vdash e' \colon t}{\Gamma, \Delta \vdash e \, e': t'} $$

$$ \frac{\Gamma, x \colon t \vdash e \colon t' }{\Gamma \vdash \lambda x\colon t. e : t \rightarrow t'} $$

I implemented the environment as a partial function from natural numbers to types and assuming extensionality as an axiom.

However, for mechanization this sort of representation is finicky because you have to work around alpha equivalence. But I have trouble figuring out how to use de Bruijn indices or levels for linear lambda calculus.

It's possible to work around this by checking types and linearity separately. I've been considering this approach for other reasons but I'm still undecided.

You could also typecheck nominally and then compile to debruijn terms. This involves a bit of duplicate code but I've been considering off other reasons.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.