*
Autosubst 2 is actively developed on GitHub:
*

- An implementation of Autosubst 2 implemented in Haskell as described in the various publications can be found at github.com/uds-psl/autosubst2
- An implementation of Autosubst 2 in OCaml is available at github.com/uds-psl/autosubst-ocaml. This implementation can be installed via opam and does not support modular syntax.
- An implementation of Autosusbt 2 in MetaCoq is available at github.com/uds-psl/autosubst-metacoq. It can be used as a command from within Coq, but for now remains a proof of concept with some missing features.

Formalising metatheory in the Coq proof assistant is tedious as native support for reasoning with binders requires a lot of uninteresting technicalities. To relieve users from so-produced boilerplate, the Autosubst framework automates working with de Bruijn terms: For each annotated inductive type, Autosubst generates a corresponding instantiation operation for parallel substitutions and a decision procedure for assumption-free substitution lemmas.

However, Autosubst is implemented in Ltac, Coq's tactic language, and thus suffers from Ltac's limitations. In particular, Autosubst is restricted to Coq and unscoped, non-mutual inductive types with a single sort of variables. In this paper, we present a new version of Autosubst that overcomes these restrictions.

Autosubst 2 is an external code generator, which translates second-order HOAS specifications into potentially mutual inductive term sorts. We extend the equational theory of Autosubst to the case of mutual inductive sorts by combining the application of multiple parallel substitutions into exactly one instantiation operation for each sort, i.e. we parallelise substitutions to vector substitutions.The resulting equational theory is both simpler and more expressive than that of the original Autosubst framework and allows us to present an even more elegant proof for the POPLMark challenge.

- POPLMark Reloaded - Link to GitHub Development.
- Algorithmic Equivalence - Online browsable version.
- POPLMark Challenge - Online browsable version.
- Weak Normalisation of call-by-value System F (unscoped) - Online browsable version.
- Weak Normalisation of call-by-value System F (scoped) - Online browsable version.
- Call-by-push-value - Online browsable version.