A well-scoped mechanisation of System F<:

Stream: computer science

[Yichen Xu]

I wanted to enrich the family of lambda calculi in cslib and share with the community a style I have been using to mechanise various type soundness results, so I just opened a PR (https://github.com/cs-lean/cslib/pull/28) adding a mechanisation of System Fsub in a home-brewed mechanisation style which I call "well-scoped". Standard progress and preservation are proven.

[Yichen Xu]

The "well-scoped" style basically combines:

• intrinsically scoped de Bruijn indices that are indexed by a "signature" describing available binders in the type context. This way, terms and types are well-formed by construction.
• Context morphisms, which are mappings between contexts that preserves typing.

I like style especially because it saves me from all the acrobatics of "pick fresh", alpha conversion and the "avoid list" in locally nameless, which are in no ways pleasant to deal with. Also, the context morphism framework provides unified theorems for context manipulation including weakening, narrowing and substitution (or any operation that satisfies the rule of a "context morphism").

These mechanisms are of course not super novel. De bruijn indices are used extensively; context morphisms are often applied in intrinsically typed proofs. But I find this combination rather satisfying to use.

[Fabrizio Montesi]

This sounds interesting, thank you! Is there any pen-and-paper presentation of this style somewhere perhaps? (No big deal if there isn't, just curious.)

[Chris Henson]

Thanks for the PR! I received your request to review and should be able to take a closer took sometime in the next few days. The biggest thing that would help would be for you to add more documentation. I see some at the top level import, but ideally every definition, theorem, inductive, etc. would be documented. As @Fabrizio Montesi says as well, a paper (or other formalizations, even in another proof assistant) you referenced is helpful for both the docs and reviewing.

[Yichen Xu]

Many thanks to you both!

regarding the documentation: right, it’s currently quite inadequate. I’ll work on enriching it over the next few days and will keep you updated.

regarding a pen-and-paper description: unfortunately no at least for this exact approach (intrinsically scoped de Bruijn indices + context morphisms). However, both ideas are well-established and appear in several places in the literature, for example:

• PLFA uses intrinsically typed representations with context morphisms.
• AutoSubst follows this approach as well.
• This early report seems to be one of the first descriptions of context morphisms.

I’m currently working on a functional pearl/experience report that discusses this "well-scoped" approach and why I find it useful. At the moment, though, I think there isn’t a pen-and-paper presentation that closely matches this particular formulation. My plan is to bring the documentation to a level where the mechanisation itself should (hopefully) be accessible on its own.