Preprints and Submissions

  1. Unfolding feasible arithmetic and weak truth, with S. Eberhard, 20 pp. Submitted for publication. [pdf]
  2. Weak theories of truth and explicit mathematics, with S. Eberhard, 31 pp. Submitted for publication. [pdf]

Journal Publications

  1. Admissible closures of polynomial time computable arithmetic, with D. Probst, Archive for Mathematical Logic 50(5-6), 2011, pp. 643-660. [pdf]
  2. Realizability in weak systems of explicit mathematics, with D. Spescha,  Mathematical Logic Quarterly 57(6), 2011, pp. 551-565. [pdf]
  3. Unfolding finitist arithmetic, with S. Feferman, Review of Symbolic Logic 3(4), 2010,  pp. 665-689. [pdf]
  4. Elementary explicit types and polynomial time operations, with D. Spescha, Mathematical Logic Quarterly 55(3), 2009, pp. 245-258. [pdf]
  5. 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]
  6. 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]
  7. Reflections on reflections in explicit mathematics, with G. Jäger, Annals of Pure and Applied Logic 136(1-2), 2005, pp. 116-133. [pdf]
  8. A proof-theoretic characterization of the basic feasible functionals, Theoretical Computer Science 329, 2004, pp. 159-176. [pdf]
  9. Theories with self-application and computational complexity, Information and Computation 185, 2003, pp. 263-297. [pdf]
  10. Wellordering proofs for metapredicative Mahlo, Journal of Symbolic Logic 67(1), 2002, pp. 260-278. [pdf]
  11. Intuitionistic fixed point theories for strictly positive operators, with Ch. Rüede, Mathematical Logic Quarterly 48(2), 2002, pp. 195-202. [pdf]
  12. 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]
  13. Fixed point theories and dependent choice, with G. Jäger, Archive for Mathematical Logic 39(7), 2000, pp. 493-508. [pdf] 
  14. The unfolding of non-finitist arithmetic, with S. Feferman, Annals of Pure and Applied Logic 104(1-3), 2000, pp. 75-96. [pdf] 
  15. 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] 
  16. 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] 
  17. Bar induction and omega model reflection, with G. Jäger, Annals of Pure and Applied Logic 97(1-3), 1999, pp. 221-230. [pdf] 
  18. 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] 
  19. Polynomial time operations in explicit mathematics, Journal of Symbolic Logic 62(2), 1997, pp. 575-594. [pdf] 
  20. 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] 
  21. Some theories with positive induction of ordinal strength phi omega 0, with G. Jäger, Journal of Symbolic Logic 61(3), 1996, pp. 818-842. [pdf] 
  22. Partial applicative theories and explicit substitutions, Journal of Logic and Computation 6(1), 1996, pp. 55-77.  [pdf] 
  23. Second order theories with ordinals and elementary comprehension, with G. Jäger, Archive for Mathematical Logic 34(6), 1995, pp. 345-375. [pdf] 
  24. Totality in applicative theories, with G. Jäger, Annals of Pure and Applied Logic 74(2), 1995, pp. 105-120. [pdf] 

Book Contributions

  1. Weak theories of operations and types, in Ways of Proof Theory, R. Schindler (Ed.), Ontos Verlag, 2010, 441-468. [pdf]
  2. 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]
  3. 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] 
  4. 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]
  5. 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

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

Edited Publications

  1. Gödel's Dialectica Interpretation, Guest Editor, Special Issue, Dialectica 62(2), 2008, pp. 145-290. [pdf]

Abstracts

  1. Weak theories of operations and types, Bulletin of Symbolic Logic 15(1), 2009, pp. 100-101.
  2. On the proof theory of type two functionals, Oberwolfach Reports 2(1), 2005, pp. 804-805.
  3. Unfolding finitist arithmetic, with S. Feferman, Bulletin of Symbolic Logic 7(1), 2001, pp. 111-112.
  4. Bounded applicative theories, Bulletin of Symbolic Logic 7(1), 2001, p. 150.
  5. Metapredicativity, Bulletin of Symbolic Logic 5(1), 1999, pp. 67-68.
  6. Aspects of metapredicativity, Bulletin of Symbolic Logic 4(1), 1998, pp. 72-73.
  7. The µ quantification operator in explicit mathematics with universes, with M. Marzetta, Bulletin of Symbolic Logic 3(1), 1997, pp. 127-128.
  8. Polynomial time operations in applicative theories, Bulletin of Symbolic Logic 3(1), 1997, pp. 105-106.
  9. 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

  1. 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.
  2. 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.
  3. Review of Andrea Cantini, Logical frameworks for truth and abstraction, Elsevier, 1996, Journal of Symbolic Logic 63(1), 1998, pp. 328-329.
  4. Numerous reviews for Mathematical Reviews.
  5. Numerous reviews for Zentralblatt Math.
A list of publications and talks in pdf-format can be downloaded here.

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