Programme – TYPES 2021

All times are in Central European Summer Time (CEST, UTC+2).

Monday

Opening
9:45 am – 10:00 am
Genuine pairs and the trouble with triples in homotopy type theory
10:00 am – 11:00 am

by Ulrik Buchholtz
Break
11:00 am – 11:30 am
Recursion
11:30 am – 12:30 pm

chair: Rasmus Ejlers Møgelberg
Lunch
12:30 pm – 1:30 pm
Inductive Types
1:30 pm – 2:00 pm

chair: Niccolò Veltri
Working Groups
2:00 pm – 2:30 pm
Break
2:30 pm – 2:45 pm
Working Groups
2:45 pm – 3:45 pm
Inductive Types
3:45 pm – 4:00 pm

chair: Niccolò Veltri

Tuesday

New Type Theories
10:00 am – 11:00 am

chair: Ambrus Kaposi
Break
11:00 am – 11:30 am
Computation and Intersection Types
11:30 am – 12:30 pm

chair: Silvia Ghilezan
Lunch
12:30 pm – 1:30 pm
Working Groups
1:30 pm – 2:45 pm
Break
2:45 pm – 3:00 pm
Session Logical Relations for Noninterference
3:00 pm – 4:00 pm

by Stephanie Balzer

Wednesday

Logical and Semantic Principles
10:00 am – 11:00 am

chair: Herman Geuvers
Break
11:00 am – 11:30 am
Model Theory
11:30 am – 12:30 pm

chair: Fredrik Nordvall Forsberg
Lunch
12:30 pm – 1:30 pm
Proof Theory
1:30 pm – 2:15 pm

chair: Delia Kesner
Break
2:15 pm – 2:30 pm
Working Groups
2:30 pm – 4:00 pm

Thursday

On the constructive content of infinitary classical theories
10:00 am – 11:00 am

by Sara Negri
Break
11:00 am – 11:30 am
Proof Assistants Foundations
11:30 am – 12:30 pm

chair: Jesper Cockx
Lunch
12:30 pm – 1:30 pm
Modal Type Theory
1:30 pm – 2:15 pm

chair: Conor McBride
Break
2:15 pm – 2:30 pm
Business Meeting
2:30 pm – 3:30 pm
Social Gathering
5:00 pm – 6:00 pm

This is open-ended. 🙂

Friday

All your base categories are belong to us
10:00 am – 11:00 am

by Pierre-Marie Pédrot
Break
11:00 am – 11:30 am
Business Meeting
11:00 am – 11:30 am
Proof Assistants Applications
11:30 am – 12:30 pm

chair: Matthieu Sozeau
Lunch
12:30 pm – 1:30 pm
Closing Discussion
1:30 pm – 2:30 pm

	Monday	Tuesday	Wednesday	Thursday	Friday
9:45 am	Opening 9:45 am – 10:00 am
10:00 am	Genuine pairs and the trouble with triples in homotopy type theory 10:00 am – 11:00 am by Ulrik Buchholtz	New Type Theories 10:00 am – 11:00 am chair: Ambrus Kaposi	Logical and Semantic Principles 10:00 am – 11:00 am chair: Herman Geuvers	On the constructive content of infinitary classical theories 10:00 am – 11:00 am by Sara Negri	All your base categories are belong to us 10:00 am – 11:00 am by Pierre-Marie Pédrot
10:15 am
10:30 am
10:45 am
11:00 am	Break 11:00 am – 11:30 am	Break 11:00 am – 11:30 am	Break 11:00 am – 11:30 am	Break 11:00 am – 11:30 am	Break 11:00 am – 11:30 am Business Meeting 11:00 am – 11:30 am
11:15 am
11:30 am	Recursion 11:30 am – 12:30 pm chair: Rasmus Ejlers Møgelberg	Computation and Intersection Types 11:30 am – 12:30 pm chair: Silvia Ghilezan	Model Theory 11:30 am – 12:30 pm chair: Fredrik Nordvall Forsberg	Proof Assistants Foundations 11:30 am – 12:30 pm chair: Jesper Cockx	Proof Assistants Applications 11:30 am – 12:30 pm chair: Matthieu Sozeau
11:45 am
12:00 pm
12:15 pm
12:30 pm	Lunch 12:30 pm – 1:30 pm	Lunch 12:30 pm – 1:30 pm	Lunch 12:30 pm – 1:30 pm	Lunch 12:30 pm – 1:30 pm	Lunch 12:30 pm – 1:30 pm
12:45 pm
1:00 pm
1:15 pm
1:30 pm	Inductive Types 1:30 pm – 2:00 pm chair: Niccolò Veltri	Working Groups 1:30 pm – 2:45 pm	Proof Theory 1:30 pm – 2:15 pm chair: Delia Kesner	Modal Type Theory 1:30 pm – 2:15 pm chair: Conor McBride	Closing Discussion 1:30 pm – 2:30 pm
1:45 pm
2:00 pm	Working Groups 2:00 pm – 2:30 pm
2:15 pm			Break 2:15 pm – 2:30 pm	Break 2:15 pm – 2:30 pm
2:30 pm	Break 2:30 pm – 2:45 pm		Working Groups 2:30 pm – 4:00 pm	Business Meeting 2:30 pm – 3:30 pm
2:45 pm	Working Groups 2:45 pm – 3:45 pm	Break 2:45 pm – 3:00 pm
3:00 pm		Session Logical Relations for Noninterference 3:00 pm – 4:00 pm by Stephanie Balzer
3:15 pm
3:30 pm
3:45 pm	Inductive Types 3:45 pm – 4:00 pm chair: Niccolò Veltri
5:00 pm				Social Gathering 5:00 pm – 6:00 pm This is open-ended. 🙂
5:15 pm
5:30 pm
5:45 pm