## Preprints and Submissions

- A flexible type system for the small Veblen ordinal, with F. Ranzi, 52 pp., submitted for publication. [pdf]

## Journal Publications

- A note on the theory SID
_{<ω}of stratified induction, with F. Ranzi, Mathematical Logic Quarterly 60(6), 2014, pp. 487-497. [pdf] - Admissible closures of polynomial time computable arithmetic, with D. Probst, Archive for Mathematical Logic 50(5-6), 2011, pp. 643-660. [pdf]
- Realizability in weak systems of explicit mathematics, with D. Spescha, Mathematical Logic Quarterly 57(6), 2011, pp. 551-565. [pdf]
- Unfolding finitist arithmetic, with S. Feferman, Review of Symbolic Logic 3(4), 2010, pp. 665-689. [pdf]
- Elementary explicit types and polynomial time operations, with D. Spescha, Mathematical Logic Quarterly 55(3), 2009, pp. 245-258. [pdf]
- Primitive recursive selection functions for existential assertions over abstract algebras, with J. I. Zucker, Journal of Logic and Algebraic Programming 76(2), 2008, pp. 175-197. [pdf]
- On the proof theory of type two functionals based on primitive recursive operations, with D. Steiner, Mathematical Logic Quarterly 52(3), 2006, pp. 237-252. [pdf]
- Reflections on reflections in explicit mathematics, with G. Jäger, Annals of Pure and Applied Logic 136(1-2), 2005, pp. 116-133. [pdf]
- A proof-theoretic characterization of the basic feasible functionals, Theoretical Computer Science 329, 2004, pp. 159-176. [pdf]
- Theories with self-application and computational complexity, Information and Computation 185, 2003, pp. 263-297. [pdf]
- Wellordering proofs for metapredicative Mahlo, Journal of Symbolic Logic 67(1), 2002, pp. 260-278. [pdf]
- Intuitionistic fixed point theories for strictly positive operators, with Ch. Rüede, Mathematical Logic Quarterly 48(2), 2002, pp. 195-202. [pdf]
- Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory, with G. Jäger, Journal of Symbolic Logic 66(2), 2001, pp. 935-958. [pdf]
- Fixed point theories and dependent choice, with G. Jäger, Archive for Mathematical Logic 39(7), 2000, pp. 493-508. [pdf]
- The unfolding of non-finitist arithmetic, with S. Feferman, Annals of Pure and Applied Logic 104(1-3), 2000, pp. 75-96. [pdf]
- The non-constructive µ operator, fixed point theories with ordinals, and the bar rule, Annals of Pure and Applied Logic 104(1-3), 2000, pp. 305-324. [pdf]
- The proof-theoretic analysis of transfinitely iterated fixed point theories, with G. Jäger, R. Kahle and A. Setzer, Journal of Symbolic Logic 64(1), 1999, pp. 53-67. [pdf]
- Bar induction and omega model reflection, with G. Jäger, Annals of Pure and Applied Logic 97(1-3), 1999, pp. 221-230. [pdf]
- The µ quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals, with M. Marzetta, Archive for Mathematical Logic 37(5+6), 1998, pp. 391-413. [pdf]
- Polynomial time operations in explicit mathematics, Journal of Symbolic Logic 62(2), 1997, pp. 575-594. [pdf]
- Systems of explicit mathematics with non-constructive µ operator and join, with Th. Glaß, Annals of Pure and Applied Logic 82(2), 1996, pp. 193-219. [pdf]
- Some theories with positive induction of ordinal strength φω0, with G. Jäger, Journal of Symbolic Logic 61(3), 1996, pp. 818-842. [pdf]
- Partial applicative theories and explicit substitutions, Journal of Logic and Computation 6(1), 1996, pp. 55-77. [pdf]
- Second order theories with ordinals and elementary comprehension, with G. Jäger, Archive for Mathematical Logic 34(6), 1995, pp. 345-375. [pdf]
- Totality in applicative theories, with G. Jäger, Annals of Pure and Applied Logic 74(2), 1995, pp. 105-120. [pdf]

## Book Contributions

- Unfolding schematic systems, in Feferman on
Foundations - Logic, Mathematics, Philosophy, G. Jäger and W. Sieg
(Eds.), Springer, 25 pp., to appear. [pdf]

- Theories of proof-theoretic strength ψ(Γ
_{Ω+1}), with U. Buchholtz and G. Jäger, in Concepts of Proof in Mathematics, Philosophy, and Computer Science, D. Probst, P. Schuster (Eds.), De Gruyter, 2016, pp. 115-140. [pdf] - Unfolding feasible arithmetic and weak truth, with S. Eberhard, in Unifying the Philosophy of Truth, D. Achourioti, H. Galinon, K. Fujimoto, J. Martinez (Eds.), Springer, pp. 153-167, 2015. [pdf]
- Weak theories of truth and explicit mathematics, with S. Eberhard, in Logic, Construction, Computation, U. Berger, H. Diener, P. Schuster, M. Seisenberger (Eds.), Ontos Verlag, 2012, pp. 157–184. [pdf]
- Weak theories of operations and types, in Ways of Proof Theory, R. Schindler (Ed.), Ontos Verlag, 2010, 441-468. [pdf]
- The proof-theoretic strength of the Suslin operator in applicative theories, with G. Jäger, in Reflections on the Foundations of Mathematics: Essays in honor of Solomon Feferman, W. Sieg, R. Sommer, C. Talcott (Eds.), ASL Lecture Notes in Logic 15, A K Peters, 2002, pp. 270-292. [pdf]
- Autonomous fixed point progressions and fixed point transfinite recursion, in Logic Colloquium ’98, S. Buss, P. Hajek, P. Pudlak (Eds.), ASL Lecture Notes in Logic 13, A K Peters, 2000, pp. 449-464. [pdf]
- First steps into metapredicativity in explicit mathematics, in Sets and Proofs, B. Cooper and J. Truss (Eds.), Cambridge University Press, 1999, pp. 383-402. [pdf]
- On applicative theories, with G. Jäger and R. Kahle, in Logic and Foundations of Mathematics, A. Cantini, E. Casari, P.L. Minari (Eds.), Kluwer, 1999, pp. 83-92. [pdf]

## Theses

- Proof-theoretic contributions to explicit mathematics, Habilitation thesis, Institute for Computer Science and Applied Mathematics, University of Berne, 2001, 163 pp. [pdf]
- On the proof theory of applicative theories, PhD thesis, Institute for Computer Science and Applied Mathematics, University of Berne, June 1996, 99 pp. [pdf]
- Theories with self-application of strength PRA, Master’s thesis, Institute for Computer Science and Applied Mathematics, University of Berne, June 1992, 86 pp.
- Aspekte des nicht-monotonen Schliessens, Minor thesis, Institute of Philosophy, University of Berne, 1990, 121 pp.

## Edited Publications

- Gödel's Dialectica Interpretation, Guest Editor, Special Issue, Dialectica 62(2), 2008, pp. 145-290. [pdf]
- Turing's Revolution: The Impact of His Ideas about Computability, with G. Sommaruga (Eds.), Birkhäuser, 329 pp., 2015. [pdf]
- Advances in Proof Theory, volume 28 of Progress in Computer
Science and Applied Logic, with R. Kahle and T. Studer (Eds.),
Birkhäuser, 2016. [pdf]

## Abstracts

- A flexible type system for the small Veblen ordinal, with F.
Ranzi, Oberwolfach Reports,
11(4), 2014, p.~2943.

- Unfolding schematic formal systems: From non-finitist to feasible
arithmetic, Bulletin of Symbolic Logic
20(3), 2014, pp. 381-382.

- Towards the unfolding of feasible arithmetic, with S. Eberhard, Bulletin of Sym-bolic Logic 18(3),
2012, pp. 474–475.

- Weak theories of operations, truth, and types, Oberwolfach Reports 8(4), 2011, pp.
2997–2998.

- Weak theories of operations and types, Bulletin of Symbolic Logic 15(1), 2009, pp. 100-101.
- On the proof theory of type two functionals, Oberwolfach Reports 2(1), 2005, pp. 804-805.
- Unfolding finitist arithmetic, with S. Feferman, Bulletin of Symbolic Logic 7(1), 2001, pp. 111-112.
- Bounded applicative theories, Bulletin of Symbolic Logic 7(1), 2001, p. 150.
- Metapredicativity, Bulletin of Symbolic Logic 5(1), 1999, pp. 67-68.
- Aspects of metapredicativity, Bulletin of Symbolic Logic 4(1), 1998, pp. 72-73.
- The µ quantification operator in explicit mathematics with universes, with M. Marzetta, Bulletin of Symbolic Logic 3(1), 1997, pp. 127-128.
- Polynomial time operations in applicative theories, Bulletin of Symbolic Logic 3(1), 1997, pp. 105-106.
- Systems of explicit mathematics with primitive recursive operations plus non-constructive µ operator, 10th International Congress of Logic, Methodology and Philosophy of Science, Florence, 1995, p. 63.

## Reviews

- Review of Katalin Bimbo, Proof Theory: Sequent calculi and
related formalisms, CRC Press, 2014, Bulletin
of Symbolic Logic 22(2), 2016, pp. 288-289.

- Review of Sergei Tupailo, Realization of analysis into explicit mathematics, Journal of Symbolic Logic 66, 2001, Bulletin of Symbolic Logic 9(1), 2003, pp. 42-43.
- Review of Andreas Weiermann, How is it that infinitary methods can be applied to finitary mathematics? Gödel’s T: a case study, Journal of Symbolic Logic 63, 1998, Bulletin of Symbolic Logic 8(3), 2002, pp. 435-436.
- Review of Andrea Cantini, Logical frameworks for truth and abstraction, Elsevier, 1996, Journal of Symbolic Logic 63(1), 1998, pp. 328-329.
- Numerous reviews for Mathematical Reviews.
- Numerous reviews for Zentralblatt Math.

Some of my publications are listed in MathSciNet, ZMATH, and DBLP.