Thursday June 14: arrivals
| arrival throughout the day | |
| 19:00—21:00 | informal gathering at Zlata Ladjica |
Friday June 15: 4WFTop tutorials
| 8:45—9:15 | registration |
| 9:15—10:00 | Thierry Coquand. Positivity in point-free topology: positivity predicates |
| 10:00—10:15 | break |
| 10:15—11:00 | Giovanni Sambin. Positivity in point-free topology: positivity relations |
| 11:00—11:15 | break |
| 11:15—12:00 | Steve Vickers. Formal Topology and Geometric Logic: spaces |
| 12:00—12:15 | break |
| 12:15—13:00 | Steve Vickers. Formal Topology and Geometric Logic: maps |
| 13:00—15:15 | lunch |
| 15:15—16:00 | Steve Vickers. Formal Topology and Geometric Logic: bundles |
| 16:00—16:15 | break |
| 16:15—17:00 | Erik Palmgren. Point-free topology and foundations of constructive analysis 1 |
| 17:00—17:15 | break |
| 17:15—18:00 | Erik Palmgren. Point-free topology and foundations of constructive analysis 2 |
Saturday June 16: 4WFTop talks
| 9:00—10:00 | Per Martin-Löf. Path models of type theory |
| 10:00—10:15 | break |
| 10:15—11:00 | Francesco Ciraulo. Binary positivity in the language of locales |
| 11:00—11:15 | break |
| 11:15—11:45 | Benno Van Den Berg. Non-deterministic inductive definitions |
| 11:45—12:15 | Tatsuji Kawai. Completeness and cocompleteness of the categories of basic pairs and concrete spaces |
| 12:15—14:15 | lunch |
| 14:15—15:00 | Bas Spitters. Locally perfect maps compose; an exercise in geometric reasoning motivated by quantum theory |
| 15:00—15:15 | break |
| 15:15—15:45 | Lurdes Sousa. Injectivity in poset enriched categories |
| 15:45—16:15 | Pietro Di Gianantonio and Abbas Edalat. A Language for Differentiable Functions |
Sunday June 17: 4WFTop talks
| 9:15—10:00 | Davorin Lešnik. Topologies in functional analysis, synthetically |
| 10:00—10:15 | break |
| 10:15—11:00 | Paul Taylor. Aspects of overtness |
| 11:00—11:15 | break |
| 11:15—11:45 | Primož Škraba. Persistent Homology – An Overview |
| 11:45—12:15 | Neža Mramor-Kosta. Discrete Morse theory |
| 12:15—14:00 | lunch |
| 14:00—19:00 | Excursion |
| 19:00—22:00 | Workshop dinner |
Monday June 18: 4WFTop talks
| 9:00—10:00 | Ieke Moerdijk. The axiom of multiple choice |
| 10:00—10:15 | break |
| 10:15—11:00 | Olivia Caramello. A topos-theoretic approach to Stone-type dualities |
| 11:00—11:15 | break |
| 11:15—11:45 | Guilhem Jaber. Intuitionistic versus Classical Forcing : A Topological Explanation |
| 11:45—12:15 | Yoshihiro Maruyama. Categorical Universal Logic: with emphasis on point-free geometric logics |
| 12:15—14:15 | lunch |
| 14:15—15:00 | Alex Simpson. Beyond the logic of observations |
| 15:00—15:15 | break |
| 15:15—15:45 | Henrik Forssell. Some applications of Moerdijk’s site description for equivariant sheaf toposes |
| 15:45—16:15 | Dirk Hofmann. Injective spaces via distributors and adjunction |
| 16:15—16:30 | break |
| 16:30—17:30 | Round table |
Tuesday June 19: 4WFTop talks
| 9:00—10:00 | Vladimir Voevodsky. Univalent fibrations |
| 10:00—10:15 | break |
| 10:15—11:00 | Claudio Sacerdoti Coen. The Kuratowski’s closure-complement problem in formal topology |
| 11:00—11:15 | break |
| 11:15—11:45 | Steve Awodey. Hopf in HoTT |
| 11:45—12:15 | Martin Escardo. The intrinsic topology of a Martin-Lof universe |
| 12:15—14:15 | lunch |
| 14:15—15:00 | Hajime Ishihara. Infinitary propositional theories and set-generated classes |
| 15:00—15:15 | break |
| 15:15—15:45 | Davide Rinaldi. A constructive notion of codimension |
| 15:45—16:15 | Martin Escardo and Chuangjie Xu. A constructive model of uniform continuity |
| 16:15—16:30 | break |
| 16:30—17:30 | Round table & Business Meeting |
Wednesday June 20: HDACT
| 9:00—10:00 | Steve Awodey. Free fibrations and singleton types |
| 10:00—10:15 | break |
| 10:15—10:45 | Francois Lamarche. Higher Homotopy Groups of Categories |
| 10:45—11:15 | Andrei Rodin. Higher Identity Types in Empirical Contexts |
| 11:15—11:30 | break |
| 11:30—12:30 | Emily Riehl. (Homotopy coherent) adjunctions of ∞-categories |
| 12:30—14:30 | lunch |
| 14:30—15:00 | Daniel R. Licata and Robert Harper. Computing with univalence |
| 15:00—15:30 | Thierry Coquand and Simon Huber. Constructive Kan Fibrations |
| 15:30—15:45 | break |
| 15:45—16:15 | Peter Aczel. What is a type theory and, what should a type theory be? |
| 16:15—16:45 | Eric Finster. Type Theory and the Opetopes |
| 16:45—17:00 | break |
| 17:00—18:00 | Thorsten Altenkirch. Towards an ω-groupoid model of Type Theory |
| 20:00—22:00 | HDACT Dinner |