Name Note Lambda Cube Affine Type Theory Linear Refinement Barendregt's Variable Convention Modal Type Theory Call by Push Value