Publications & Preprints

No. Author(s) Title Preprint
(arXiv)
Publication
(MathSciNet)
2018b01 Petrakis, I. Dependent sums and dependent products in Bishop's set theory Preprint 24th International Conference on Types for Proofs and Programs, Leibniz International Proceedings in Informatics (LIPIcs), doi: 10.4230/LIPIcs.TYPES.2018.3
2018b02 Afshari, B.; Jäger, G.; Leigh, G.E. An Infinitary Treatment of Full Mu-Calculus   MR3976067
2018b03 Arai, T.; Fernandez-Duque, D.; Wainer, S.; Weiermann, A. Predicatively unprovable termination of the Ackermannian Goodstein process 1906.00020  
2018b04 Bezem, M.; Coquand, T. Skolem’s Theorem in Coherent Logic   MR4028053
2018b05 Centrone, S.; Negri, S.; Sarikaya, D.; Schuster, P. (eds.) Mathesis Universalis, Computability and Proof   Springer (2019), doi: 10.1007/978-3-030-20447-1
2018b06 Dalmonte, T.; Olivetti, N.; Negri, S. Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi   MR3839114
2018b07 Krombholz, M.; Rathjen, M. Upper bounds on the graph minor theorem 1907.00412 In: Schuster, P.; Seisenberger, M.; Weiermann, A. (eds.) Well-Quasi Orders in Computation, Logic, Language and Reasoning. Trends in Logic (Studia Logica Library), vol 53. Springer (2020), Cham, doi: 10.1007/978-3-030-30229-0_6
2018b08 Negri, S.; Orlandelli, E. Proof theory for quantified monotone modal logics   MR3989541
2018b09 Niki, S.; Schuster, P. On Scott's Semantics for Many-Valued Logic   submitted
2018b10 Powell, T.; Schuster, P.; Wiesnet, F. An algorithmic approach to the existence of ideal objects in commutative algebra 1903.03070 MR39760972
2018b11 Rathjen, M.; Sieg, W. Proof Theory   The Stanford Encyclopedia of Philosophy (Fall 2018 Edition), Edward N. Zalta (ed.)
2018b12 Rathjen, M.; Thomson, I.A. Well-ordering principles, ω-models and Π11-comprehension   to appear in: The legacy of Kurt Schütte, edited by K. Kahle et al. (in press)
2018b13 Rathjen, M.; Toppel, M. On relating theories: Proof-theoretical reduction   In: Centrone, S.; Negri, S.; Sarikaya, D.; Schuster, P. (eds.) Mathesis Universalis, Computability and Proof, Springer (2019), doi: 10.1007/978-3-030-20447-1
2018b14 Rathjen, M.; Tupailo, S. On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics   to appear in: The legacy of Kurt Schütte, edited by K. Kahle et al. (in press)
2018b15 Schwichtenberg, H. Program extraction from proofs: the fan theorem for uniformly coconvex bars   In: Centrone, S.; Negri, S.; Sarikaya, D.; Schuster, P. (eds.) Mathesis Universalis, Computability and Proof, Springer (2019), doi: 10.1007/978-3-030-20447-1
2018b16 Schwichtenberg, H.; Wiesnet, F. Logic for exact real arithmetic 1904.12763 submitted to CCC19
2018b17 Sieg, W. The Cantor-Bernstein theorem: how many proofs?   MR3917524
2018b18 Sieg, W.; Walsh, P. Natural formalization: Proving the Cantor-Bernstein Theorem in ZF   The Review of Symbolic Logic (2019), doi: 10.1017/S175502031900056X
2018b19 Bridges, D.S. Intuitionistic sequential compactness?   MR3860871
2018b20 Bridges, D.S.; Hendtlass, M. Constructive mathematical economics   to appear in: Bridges, D.; Ishihara, H.; Rathjen, M.; Schwichtenberg, H. (eds.) Handbook of Constructive Mathematics
2018b21 Coquand, T. A survey of constructive presheaf models of univalence   ACM SIGLOG News (2018), doi: 10.1145/3242953.3242962
2018b22 Coquand, T.; Lombard, H.; Neuwirth, S. Lattice-ordered groups generated by an ordered group and regular systems of ideals 1701.05115 MR4010570
2018b23 Schlagbauer, K.; Schuster, P.; Wessel, D. Der Satz von Hahn–Banach per Disjunktionselimination   MR4002395
2018b24 Fellin, G.; Schuster, P.; Wessel, D. The Jacobson Radical of a Propositional Theory Preprint submitted
2018b25 Gamanda, M.; Lombardi, H.; Neuwirth, S; Yengui, I. The syzygy theorem for Bézout rings 1905.08117 MR4044457
2018b26 Schuster, P.; Wessel, D.; Yengu, I. Dynamic evaluation of integrity and the computational content of Krull’s lemma   submitted
2018b27 Schwichtenberg, H. Computational aspects of Bishop’s constructive mathematics   to appear in: Bridges, D.; Ishihara, H.; Rathjen, M.; Schwichtenberg, H. (eds.) Handbook of Constructive Mathematics
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-1096374442
2018b29 Wessel, D. Point-free spectra of linear spreads   In: Centrone, S.; Negri, S.; Sarikaya, D.; Schuster, P. (eds.) Mathesis Universalis, Computability and Proof, Springer (2019), doi: 10.1007/978-3-030-20447-1
2018b30 Gambino, N.; Henry, S. Towards a constructive simplicial model of Univalent Foundations 1905.06281  
2018b31 Gambino, N.; Larrea, M.F. Models of Martin-Löf type theory from algebraic weak factorisation systems 1906.01491  
2018b32 Sieg, W.; Derakhshan, F. Human-oriented automated proof search Preprint  
2018b33 Xu, C. A syntactic approach to continuity of T-definable functionals 1904.09794  
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  
2018b36 Berger, J.; Svindland, G. Constructive Proofs of Negated Statements   In: Centrone, S., Negri, S., Sarikaya, D., Schuster, P.M. (Eds.) Mathesis Universalis, Computability and Proof Springer (2019), doi: 10.1007/978-3-030-20447-1
2018b37 Berger, J. The fan theorem 2001.00064  
2018b38 Berger, J.; Svindland, G. Brouwer's fan theorem and convexity   MR3893278
2018b39 Berger, U.; Matthes, R.; Setzer, A. Martin Hofmann's Case for Non-Strictly Positive Data Types   24th International Conference on Types for Proofs and Programs, doi: 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   In: Proceedings of the ACM on Programming Languages, January 2019, Article No.: 23; doi: https://doi.org/10.1145/3290336
2018b43 Paul-André, M. Template games and differential linear logic   In: 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2019)
2018b44 Maietti, M.; Maschio, S.; A predicative variant of Hyland's Effective Topos 1806.08519  
2018b45 Maietti, M.; Pasquali, F.; Rosolini, G.; Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies 1802.06400 In: Logical Methods in Computer Science, Volume 15, Issue 2 (June 25, 2019) lmcs:5597, doi: 10.23638/LMCS-15(2:21)2019
2018b46 Freund, A. Pi^1_1-Comprehension as a Well-Ordering Principle 1809.06759 MR3994445
2018b47 Freund, A. A Categorical Construction of Bachmann-Howard Fixed Points 1809.06769 MR4022428
2018b48 Freund, A. Computable Aspects of the Bachmann-Howard Principle 1809.06774 to appear in the Journal of Mathematical Logic, doi:10.1142/S0219061320500063
2018b49 Moschovakis, J.R. Calibrating the negative interpretation   contributed talk at 12th Panhellenic Logic Symposium, 2019