A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL

The theory files and proof scripts for this paper are as follows.

Linear and non-linear types: Types.thy, Types.ML.

Linear and non-linear types: Types.thy, Types.ML.

Untyped environments: Env.thy, Env.ML.

Typed environments: TypedEnv.thy, TypedEnv.ML.

The meta language: Meta.thy, Meta.ML.

The typed meta language: TypedMeta.thy, TypedMeta.ML.

Substitution: Subst.thy, Subst.ML.

The linear pi calculus: Pi.thy, Pi.ML.

Additional tactics: Tactics.thy, Tactics.ML.