Cong will give a lecture on dependently typed programming in Agda at PPL Summer School 2025, affiliated with the 42nd JSSST annual conference.
The materials for the lecture can be found on GitHub.
