May 2 - August 24, 2018
Organizers: Douglas S. Bridges, Michael Rathjen, Peter Schuster, Helmut Schwichtenberg
Description: Type theory, originally conceived as a bulwark against the paradoxes of naive set theory, has languished for a long time in the shadow of axiomatic set theory which became the mainstream foundation of mathematics. The first renaissance of type theory occurred with the advent of computer science and Bishop's development of a practice-oriented constructive mathematics. It was followed by a second quite recent one that not only champions type theory as a central framework for achieving the goal of fully formalized mathematics amenable to verification by computer-based proof assistants, but also finds deep and unexpected connections between type theory and homotopy theory. Constructive set theory and mathematics distinguishes itself from its traditional counterpart, classical set theory and mathematics based on it, by insisting that proofs of existential theorems must afford means for constructing an instance. Constructive reasoning emerges naturally in core areas of mathematics and in the theory of computation. The aim of the Hausdorff Trimester is to create a forum for research on and dissemination of exciting recent developments, which are of central importance to modern foundations of mathematics.
Associated Events: The program will include the following events:
- Summer School, addressed to PhD students and postdocs (May 3-9, 2018, without Sunday, 6th)
Three major workshops
- Types, Homotopy Type theory, and Verification (June 4 - June 8)
- Proofs and Computation (July 2 - July 6)
- Constructive Mathematics (August 6 - August 10)
Those planning to participate include: Peter Aczel, Toshiyasu Arai, Sergei Artemov, Steve Awodey, Andrej Bauer, Ulrich Berger, Thierry Coquand, Martín Escardó, Rosalie Iemhoff, Hajime Ishihara, Gerhard Jäger, Peter Koellner, Ulrich Kohlenbach, Robert Lubarsky, Maria Emilia Maietti, Per Martin-Löf, Paul-André Mellies, Sara Negri, Paulo Oliva, Erik Palmgren, Giuseppe Rosolini, Giovanni Sambin, Monika Seisenberger, Andreas Weiermann, Ihsen Yengui
© HIM
| No. | Author(s) | Title | Preprint | Publication |
| 2018b01 | Petrakis, I. | Dependent Sums and Dependent Products in Bishop's Set Theory | Leibniz International Proceedings in Informatics. 130 (2019), 3:1-3:21. https://doi.org/10.4230/LIPIcs.TYPES.2018.3 |
|
| 2018b02 | Afshari, B.; Jäger, G.; Leigh, G.E. | An Infinitary Treatment of Full Mu-Calculus | Lecture Notes in Computer Science. 11541 (2019). https://doi.org/10.1007/978-3-662-59533-6_2 |
|
| 2018b03 | Arai, T.; Fernandez-Duque, D.; Wainer, S.; Weiermann, A. | Predicatively Unprovable Termination of the Ackermannian Goodstein Process | 1906.00020 | Proc. Amer. Math. Soc. 148 (2020), 3567-3582. https://doi.org/10.1090/proc/14813 |
| 2018b04 | Bezem, M.; Coquand, T. | Skolem’s Theorem in Coherent Logic | Fund. Inform. 170(1-3) (2019), 1–14. http://dx.doi.org/10.3233/FI-2019-1853 |
|
| 2018b05 | Centrone, S.; Negri, S.; Sarikaya, D.; Schuster, P. (eds.) | Mathesis Universalis, Computability and Proof | Springer (2019). 10.3233/FI-2019-1853 |
|
| 2018b06 | Dalmonte, T.; Olivetti, N.; Negri, S. | Non-Normal Modal Logics: Bi-Neighbourhood Semantics and its Labelled Calculi | Advances in Modal Logic. (2018). hal-02076639 |
|
| 2018b07 | Krombholz, M.; Rathjen, M. | Upper Bounds on the Graph Minor Theorem | 1907.00412 | Trends in Logic. 53. https://doi.org/10.1007/978-3-030-30229-0_6 |
| 2018b08 | Negri, S.; Orlandelli, E. | Proof Theory for Quantified Monotone Modal Logics | Logic Journal of the IGPL. 27(4) (2019), 478–506. https://doi.org/10.1093/jigpal/jzz015 |
|
| 2018b09 | Niki, S.; Schuster, P. | On Scott's Semantics for Many-Valued Logic | Journal of Logic and Computation. 30(6) (2020), 1291–1302. https://doi.org/10.1093/logcom/exaa036 |
|
| 2018b10 | Powell, T.; Schuster, P.; Wiesnet, F. | An Algorithmic Approach to the Existence of Ideal Objects in Commutative Algebra | Lecture Notes in Computer Science. 11541. https://doi.org/10.1007/978-3-662-59533-6_32 |
|
| 2018b11 | Rathjen, M.; Sieg, W. | Proof Theory | The Stanford Encyclopedia of Philosophy. (2018),Edward N. Zalta (ed.) |
|
| 2018b12 | Rathjen, M.; Thomson, I.A. | Well-Ordering Principles, ω-Models and Π11-Comprehension | The Legacy of Kurt Schütte. https://doi.org/10.1007/978-3-030-49424-7_12 |
|
| 2018b13 | Rathjen, M.; Toppel, M. | On Relating Theories: Proof-Theoretical Reduction | Mathesis Universalis, Computability and Proof. Synthese Library, 412. https://doi.org/10.1007/978-3-030-20447-1_16 |
|
| 2018b14 | Rathjen, M.; Tupailo, S. | On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics | The Legacy of Kurt Schütte. https://doi.org/10.1007/978-3-030-49424-7_19 |
|
| 2018b15 | Schwichtenberg, H. | Program Extraction from Proofs: The Fan Theorem for Uniformly Coconvex Bars | Mathesis Universalis, Computability and Proof. Synthese Library, 412. https://doi.org/10.1007/978-3-030-20447-1_17 |
|
| 2018b16 | Schwichtenberg, H.; Wiesnet, F. | Logic for Exact Real Arithmetic | 1904.12763 | Mathematics for Computation (M4C). (2023), 39-69 https://doi.org/10.1142/9789811245220_0003 |
| 2018b17 | Sieg, W. | The Cantor-Bernstein Theorem: How Many Proofs? | Phil. Trans. R. Soc. A. 377. http://dx.doi.org/10.1098/rsta.2018.0031 |
|
| 2018b18 | Sieg, W.; Walsh, P. | Natural Formalization: Proving the Cantor-Bernstein Theorem in ZF | The Review of Symbolic Logic. 14(1) (2021), 250–84. https://doi.org/10.1017/S175502031900056X |
|
| 2018b19 | Bridges, D.S. | Intuitionistic Sequential Compactness? | Indagationes Mathematicae. 29(6) (2018), 1477-149, https://doi.org/10.1016/j.indag.2017.10.011 |
|
| 2018b20 | Bridges, D.S.; Hendtlass, M. | Constructive Mathematical Economics | In Handbook of Constructive Mathematics. (2023), 302–32. Encyclopedia of Mathematics and Its Applications. https://doi.org/10.1017/9781009039888.013 |
|
| 2018b21 | Coquand, T. | A Survey of Constructive Presheaf Models of Univalence | ACM SIGLOG News. 5(3), 54 - 65. https://doi.org/10.1145/3242953.3242962 |
|
| 2018b22 | Coquand, T.; Lombard, H.; Neuwirth, S. | Lattice-Ordered Groups Generated by an Ordered Group and Regular Systems of Ideals | Rocky Mountain J. Math. 49(5) (2019), 1449 - 1489. https://doi.org/10.1216/RMJ-2019-49-5-1449 |
|
| 2018b23 | Schlagbauer, K.; Schuster, P.; Wessel, D. | Der Satz von Hahn–Banach per Disjunktionselimination | Confluentes Mathematici. 11(1) (2019), 79-93. 10.5802/cml.57 |
|
| 2018b24 | Fellin, G.; Schuster, P.; Wessel, D. | The Jacobson Radical of a Propositional Theory | Preprint | The Bulletin of Symbolic Logic. 28(2) (2022), 163–81. https://doi.org/10.1017/bsl.2021.66 |
| 2018b25 | Gamanda, M.; Lombardi, H.; Neuwirth, S; Yengui, I. | The Syzygy Theorem for Bézout Rings | 1905.08117 | Math. Comp. 89 (2020), 941-964. https://doi.org/10.1090/mcom/3466 |
| 2018b26 | Schuster, P.; Wessel, D.; Yengu, I. | Dynamic Evaluation of Integrity and the Computational Content of Krull’s Lemma | Journal of Pure and Applied Algebra. 226(1) (2022). https://doi.org/10.1016/j.jpaa.2021.106794 |
|
| 2018b27 | Schwichtenberg, H. | Computational Aspects of Bishop’s Constructive Mathematics | In Handbook of Constructive Mathematics. (2023), 715–48. Encyclopedia of Mathematics and Its Applications. https://doi.org/10.1017/9781009039888.027 |
|
| 2018b28 | Yengui, I. | Computational Commutative Algebra and Algebraic Geometry: Course and Exercises with Detailed Solutions | Kindle Direct Publishing. (2019). ISBN-10: 1096374447, ISBN-13: 978 https://hal.science/hal-02150072 |
|
| 2018b29 | Wessel, D. | Point-Free Spectra of Linear Spreads | Computability and Proof. Synthese Library. 412. https://doi.org/10.1007/978-3-030-20447-1_19 |
|
| 2018b30 | Gambino, N.; Henry, S. | Towards a Constructive Simplicial Model of Univalent Foundations | 1905.06281 | J. of the London Math. Society. 105(2) (2022), 709-1361, https://doi.org/10.1112/jlms.12532 |
| 2018b31 | Gambino, N.; Larrea, M.F. | Models of Martin-Löf Type Theory from Algebraic Weak Factorisation Systems | 1906.01491 | The Journal of Symbolic Logic. 88(1) (2023), 242–89. https://doi.org/10.1017/jsl.2021.39 |
| 2018b32 | Sieg, W.; Derakhshan, F. | Human-Oriented Automated Proof Search | Autom Reasoning. 65 (2021), 1153–1190. https://doi.org/10.1007/s10817-021-09594-z |
|
| 2018b33 | Xu, C. | A Syntactic Approach to Continuity of T-Definable Functionals | 1904.09794 | Logical Methods in Computer Science. 16(1) (2020). https://doi.org/10.23638/LMCS-16(1:22)2020 |
| 2018b33 | Natingga, D. | α Degrees as an Automorphism Base for the α-Enumeration Degrees | 1812.11308 | |
| 2018b34 | Natingga, D. | Embedding Theorem for the Automorphism Group of the α-Enumeration Degrees | PhD thesis | |
| 2018b35 | Lubarsky, R.S. | Inner and Outer Models for Constructive Set Theories | Preprint | In Handbook of Constructive Mathematics, (2023), 584–635. Encyclopedia of Mathematics and Its Applications. https://doi.org/10.1017/9781009039888.023 |
| 2018b36 | Berger, J.; Svindland, G. | Constructive Proofs of Negated Statements | Mathesis Universalis, Computability and Proof. 412. https://doi.org/10.1007/978-3-030-20447-1_5 |
|
| 2018b37 | Berger, J. | Brouwer's fan theorem | 2001.00064 | |
| 2018b38 | Berger, J.; Svindland, G. | Brouwer's fan theorem and convexity | The Journal of Symbolic Logic. 83(4) (2018), 1363 - 1375. https://doi.org/10.1017/jsl.2018.49 |
|
| 2018b39 | Berger, U.; Matthes, R.; Setzer, A. | Martin Hofmann's Case for Non-Strictly Positive Data Types | Leibniz Inter. Proceedings in Informatics. 130 (2019), 1:1-1:22. https://doi.org/10.4230/LIPIcs.TYPES.2018.1 |
|
| 2018b40 | Altman, H.; Weiermann, A. | Maximum Linearizations of Lower Sets in N^m with Application to Monomial Ideals | 1909.06719 | |
| 2018b41 | Gordeev, L. | Predicative Proof Theory of PDL and Basic Applications | 1904.05131 | |
| 2018b42 | Paul-André, M. | Categorical Combinatorics of Synchronization and Scheduling in Game Semantics | Proceedings of the ACM on Programming Languages. 3(23), 1-30. https://doi.org/10.1145/3290336 |
|
| 2018b43 | Paul-André, M. | Template Games and Differential Linear Logic | 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). (2019), 1-13. 10.1109/LICS.2019.8785830 |
|
| 2018b44 | Maietti, M.; Maschio, S.; | A Predicative Variant of Hyland's Effective Topos | 1806.08519 | The Journal of Symbolic Logic. 86(2) (2021), 433–47. https://doi.org/10.1017/jsl.2020.49 |
| 2018b45 | Maietti, M.; Pasquali, F.; Rosolini, G.; | Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies | 1802.06400 | Logical Methods in Computer Science. 15(2) (2019), 21:1–21:21. https://lmcs.episciences.org |
| 2018b46 | Freund, A. | Pi^1_1-Comprehension as a Well-Ordering Principle | Advances in Mathematics. 355 (2019). https://doi.org/10.1016/j.aim.2019.106767 |
|
| 2018b47 | Freund, A. | A Categorical Construction of Bachmann-Howard Fixed Points | 1809.06769 | Bull. London Math. Soc. 51 (2019), 801–814. doi:10.1112/blms.12285 |
| 2018b48 | Freund, A. | Computable Aspects of the Bachmann-Howard Principle | 1809.06774 | J. Math. Log. 20(2) (2020), 26 pp. https://doi.org/10.1142/S0219061320500063 |
| 2018b49 | Moschovakis, J.R. | Calibrating the Negative Interpretation | 12th Panhellenic Logic Symposium. Anogeia, Crete June 26-30, 2019 |
|
| 2018b50 | Emmenegger, J.; Pasquali, F.; Rosolini, G. | Elementary Doctrines as Coalgebras | Journal of Pure and Applied Algebra. 224(12) (2020). https://doi.org/10.1016/j.jpaa.2020.106445 |
|
| 2018b51 | Kahle, R. | A Logician's Sidelong Glance at Irony | Baltic International Yearbook of Cognition, Logic and Communication. 12. https://doi.org/10.4148/1944-3676.1117 |
| Name | Affiliation |
| Peter Aczel | Munstar University |
| Bahareh Afshari | University of Gothenburg |
| Amirhossein Akbar Tabatabai | Czech Academy of Sciences |
| Sergei Artemov | CUNY Graduate Center |
| Steve Awodey | Carnegie Mellon University |
| Josef Berger | Ludwig-Maximilians-Universität München |
| Ulrich Berger | Swansea University |
| Ingo Blechschmidt | Universität Augsburg |
| Nuria Brede | Universität Potsdam |
| Douglas S. Bridges | University of Canterbury |
| Pieter Collins | Maastricht University |
| Thierry Coquand | Goteborg University |
| Anupam Das | University of Copenhagen |
| Hannes Diener | University of Canterbury |
| Peter Dybjer | Chalmers University of Technology |
| Jacopo Emmenegger | Stockholms Universitet |
| David Fernández-Duque | Ghent University |
| Anton Freund | TU Darmstadt |
| Jonas Frey | Carnegie Mellon University |
| Makoto Fujiwara | Waseda University |
| Philipp Haselwarter | University of Ljubljana |
| Matthew Hendtlass | University of Canterbury |
| Hugo Herbelin | University Paris Diderot |
| Simon Huber | University of Gothenburg |
| John Martin Elliott Hyland | University of Cambridge |
| Martin Hötzel Escardó | University of Birmingham |
| Rosalie Iemhoff | Utrecht University |
| Hajime Ishihara | Japan Advanced Institute of Science and Technology |
| Raheleh Jalali Keshavarz | Czech Academy of Sciences |
| Gerhard Jäger | Universität Bern |
| Reinhard Kahle | CMA & DM, FCT, Universidade Nova de Lisboa |
| Tatsuji Kawai | Japan Advanced Institute of Science and Technology |
| Peter Koellner | Harvard University |
| Ulrich Kohlenbach | Technische Universität Darmstadt |
| Nils Köpp | Ludwig-Maximilians-Universität München |
| Graham Leigh | University of Gothenburg |
| Dan Licata | Wesleyan University |
| Robert Lubarsky | Florida Atlantic University |
| Maria Emilia Maietti | University of Padova |
| Ralph Matthes | IRIT - Université Paul Sabatier |
| Paul-André Melliès | CNRS |
| Anders Mörtberg | Carnegie Mellon University |
| Dávid Natingga Tóth | University of Leeds |
| Sara Negri | University of Helsinki |
| Takako Nemoto | Japan Advanced Institute of Science and Technology |
| Stefan Neuwirth | Université de Franche-Comté |
| Satoru Niki | Japan Advanced Institute of Science and Technology |
| Isabel Maria Oitavem | CMA & DM, FCT, Universidade Nova de Lisboa |
| Erik Palmgren | Stockholm University |
| Dirk Pattinson | The Australian National University |
| Anja Petkovic | University of Ljubljana |
| Iosif Petrakis | Ludwig-Maximilians-Universität München |
| Olga Petrovska | Swansea University |
| Michael Rathjen | University of Leeds |
| Giuseppe Rosolini | Universit� degli Studi di Genova |
| Giovanni Sambin | University of Padova |
| Masahiko Sato | Kyoto University |
| Masahiko Sato | Kyoto University |
| Peter Schuster | Università degli Studi di Verona |
| Helmut Schwichtenberg | Ludwig-Maximilians-Universität München |
| Monika Seisenberger | Swansea University |
| Christoph-Simon Senjak | Universität Freiburg |
| Anton Setzer | Swansea University |
| Wilfried Sieg | Carnegie Mellon University |
| Andrei Sipos | Technische Universität Darmstadt |
| Bas Spitters | Aarhus University |
| Dieter Spreen | Universität Siegen |
| Andrew Swan | |
| Tsutomu Takayama | Kyoto University |
| Davide Trotta | University of Trento |
| Hideki Tsuiki | Kyoto University |
| Floris van Doorn | Worcester Polytechnic Institute |
| Jan Fhr. von Plato | University of Helsinki |
| Andreas Weiermann | Ghent University |
| Felix Wellen | Carnegie Mellon University |
| Daniel Wessel | Università degli Studi di Verona |
| Franziskus Wiesnet | Università degli Studi di Verona |
| Chuangjie Xu | Ludwig-Maximilians-Universität München |
| Ihsen Yengui | Università degli Studi di Verona |
© HIM