Quotients by Idempotent Functions in Cedille.- Early Experience in Teaching the Basics of Functional Language Design with a Language Type Checker.- Verifying Selective CPS Transformation for Shift and Reset.- How to Specify it! A Guide to Writing Properties of Pure Functions.- Type Inference for Rank 2 Gradual Intersection Types.- Set Constraints, Pattern Match Analysis, and SMT.