This repository is meant to contain various Agda formalizations in Agda of πLIN, a version of the linear π-calculus based on linear logic. full CP with exponentials and polymorphism finite types and processes infinite types and processes (planned)