Design and Implementation of the Andromeda Proof Assistant

*** PLEASE NOTE THAT WE ARE MEETING ON SUNDAY, NOT SATURDAY ***

What kinds of type theories lie beyond the bounds of our galaxy? We may never find out, but we can read Design and Implementation of the Andromeda Proof Assistant by Andrej Bauer et al (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.5), and then get together to discuss it..

We'll meet over Zoom and post the meeting URL here a few minutes before meeting start time.