Schedule.2019

Schedule of the academic year 2019/20

LP1/2 (Sep–Dec 2019):

• EDIT Analysen booked 26 September – 19 December.
• Exceptions:
  • EDIT 8103 on 3 Oct, 21 Nov, 28 Nov and 5 Dec.

Date	Leader	Topic	Remark
26 Sep	_	Planning	EDIT Analysen
3 Oct	Jesper	How to formalize stuff in Agda	EDIT 8103; Absent: Andreas
10 Oct	Jesper	Hackathon: Correct by Construction Programming in Agda	Absent: Sandro, Andreas
17 Oct	Andreas	STLC and CCCs
24 Oct	Sandro	Moggi's Computational Lambda Calculus and Monads
31 Oct	Sandro	Gray-Box Monitoring of Hyperproperties	Exams
7 Nov	Abraham Wolk	Constructive mathematics and computer programming	Absent: Nachi
14 Nov	Jesper	Observational equality, now!	Absent: Nachi, Carlos
21 Nov	_	_	No meeting
28 Nov	Jannis	MSc thesis: A reflexive graph model for sized types	EDIT 8103
5 Dec	Cătălin Hrițcu	When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise	At 14:00, Room ES52
12 Dec	Andreas, Nachi	From syntax to semantics and back: Demystifying NbE	NbE course presentation
19 Dec	_	_	No meeting

LP3/4 (Jan–Jun 2020):

• EDIT Analysen booked 16 January – 18 June.
• Exceptions:
  • EDIT 8103 on 30 January and 16 April.

Date	Leader	Topic	Remark
16 Jan	_	Planning	Absent: Andreas
23 Jan	Peter Dybjer	Categories with Families: Unityped, Simply Typed, and Dependently Typed
30 Jan	Riccardo	On the impact of semantics in functional optimizing compilers	EDIT 8103
6 Feb	Matthí	Abstract Interpretation
13 Feb	Joel	Kan extensions: the big picture of limits and colimits
20 Feb	Carlos	Modalities, Cohesion and Information Flow
27 Feb	Mattias	Set Theory	Stockholm-Göteborg type theory seminar in EDIT 8103
5 Mar	_	_	No meeting. EWSCS
12 Mar	Ana Bove	Partiality and general recursion in type theory
19 Mar	_	Preparatory Reading: Call-By-Push-Value	Postponed due to COVID-19. Exams
26 Mar	Andreas	Normalization by Evaluation for Call-By-Push-Value	Postponed due to COVID-19
2 Apr	Nachi	Categorical Combinators	Postponed due to COVID-19
9 Apr	_	Reading Session: Call-By-Push-Value (I)	On Zoom
16 Apr	_	Reading Session: Call-By-Push-Value (II)	On Zoom
23 Apr	Nachi	Categorical Combinators	On Zoom. MGS (cancelled)
30 Apr	Frederik Hanghøj Iversen	Univalent Categories — A formalization of category theory in Cubical Agda	On Zoom. Halvdag
7 May	_	_	No meeting
14 May	_	_	No meeting
21 May	_	_	Public holiday
28 May	Alexander Fuhs	Verified Compilation to Intrinsically Typed Control-Flow Graphs in Agda	On Zoom. EPIT (cancelled)
4 Jun	_	_	Exams. No meeting. AIM XXXII
11 Jun	_	_	No meeting. Epigram 2 — Autopsy, Obituary, Apology
18 Jun	Robin Adams	String Diagrams	On Zoom (postponed)
25 Jun	_	Casual meeting	On Zoom. Last meeting before summer. NLS (cancelled)

Summer break (Jul–Aug 2020):

Date	Leader	Topic	Remark
2–9 Jul	_	_	Summer break. OPLSS (cancelled)
16–23 Jul	_	_	Summer break. DeepSpec
30 Jul	_	_	Summer break. UniMath
6–13 Aug	_	_	Summer break. ESSLLI (cancelled)