Hello,
at the meeting on Wednesday Thierry and Ulf will talk about
Agda-light (language and implementation) and the connection to a FOL-prover
that Ulf has implemented.
The meeting is at 13.15 in the room next to the post-room.
Regards
Catarina