This SNSF-funded project is concerned with fixed points, recursive definitions, and proofs by induction, which are essential concepts in mathematics and computer science.
In recent years, a novel approach to formal proofs representing concepts of this kind has become popular, namely non-wellfounded and cyclic proofs. These proofs not only derive propositions from axioms, but they also provide a formal counterpart to proofs by infinite descent, i.e. proof branches that are not well-founded but satisfy some global soundness condition.
In this project, we aim for a better understanding of the structural properties of non-wellfounded and cyclic proof systems.

Candidates should hold or expect a PhD and have a strong background in logic.

We offer a stimulating research environment in an international research group. The University of Bern conducts excellent research and lives up to its vision that knowledge generates value. Bern is ideally located in the middle of Switzerland and Europe, providing rich cultural and outdoor activities.

Applications should include:
1) A cover letter detailing research interests and fit for the position.
2) A curriculum vitae including a list of publications / preprints.
3) A research proposal (max 2 pages) outlining your proposed ideas in the areas mentioned above.
4) Contact information for two references.

The complete application should be sent by e-mail to Prof. Thomas Studer at thomas.studer@unibe.ch

Applications submitted by October 17, 2025 will receive full consideration.