In this seminar, I will present my current research about contextual type inference, which generalises the bidirectional typing and allows partial type information propagation. I will also showcase two versions of type systems both in a declarative and algorithmic way. Their soundness and completeness have been proven in Agda. I will also discuss some potential applications if time allows.

We will set up the zoom and send the link to the slack before the session starts.