Re: [TYPES] TaPL Course?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Robert,

We have a Formal Systems course based on TAPL at KU Leuven.
In 2 practical sessions, the students learn how to use Agda and in the 
third, they formalize Typed Arithmetic:
https://urldefense.com/v3/__https://github.com/anuyts/agda-sessions__;!!IBzWLUs!VVdQCimkUObVjDW1CI1V2_kcHewEmae7Ry_alrqCQq6XESgAi54MWeKWEj0mO12hy2avYusU0aEvQachzxrmpFnznjbhMvi3JQ$ 
There's also a course project. It used to be a formalization of various 
extensions of the STLC but now we're formalizing Web Assembly instead.

Best,
Andreas Nuyts

On 01.12.22 06:49, Robert Rand wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hi,
>
> I was wondering who is teaching a programming languages course using Types
> and Programming Languages? I'm planning on teaching such a course at
> UChicago this Spring (March - June) and I'm looking for inspiration and
> suggestions. If you're on the quarter system and/or have material you'd
> like to share, that's especially welcome!
>
> Thanks!
> Robert