**TopTT : Topology for Types and Terms**
**[ANR](https://www.anr.fr) "Young Researcher" (JCJC) project, 2024-2028**
**[IRIF](https://www.irif.fr), [Université Paris Cité](https://www.u-paris.fr)**
A **12-month post-doctoral position in topology, algebra, categories and logic** is available at the CNRS, located at the research institute [IRIF](https://www.irif.fr) of CNRS and Université Paris Cité.
The position is financed by the ANR (French National Research Agency) project *Topology for Types and Terms*, coordinated by [Sam van Gool](https://www.samvangool.net), [vangool@irif.fr](vangool@irif.fr). Any candidate with a PhD in mathematics or computer science and a scientific interest in the project's topics is encouraged to apply.
The application should contain a motivation letter, an academic CV, and the contact information of two academic references (name, e-mail, and connection to the applicant). It can be submitted via
https://emploi.cnrs.fr/Offres/CDD/UMR8243-OMUAVC-005/Default.aspx?lang=EN
**Deadline: 17 May 2024**
Expected start date: 1 September 2024 (negotiable)
Any candidate intending to submit an application is also encouraged to express their interest via e-mail to the project coordinator as soon as possible.
**Project description.** Logic is a theme common to both the theory of automata and the study of programming languages. In the theory of automata and circuits, logic is typically used as a descriptive formalism to classify complexity classes. In the proof-theoretic study of programming languages, on the other hand, logic is used mostly for reasoning about behavioral properties of computational systems, such as their use of resources, or their treatment of higher-order functions and fixpoints. This project will use profinite topological methods to develop a common foundation for these two distinct uses of logic.
The research in this project is organized around three work packages, involving (1) profinite type spaces for finite model theory; (2) syntactic and semantic methods for logics with fixed points; (3) categorical and sheaf-theoretic methods for higher order logics and automata.
The project runs from January 2024 until December 2027 and takes place at [IRIF](https://www.irif.fr), a research institute on the foundations of computer science of the [CNRS](https:/www.cnrs.fr) and [Université Paris Cité](https://www.u-paris.fr). The project's themes naturally fit with IRIF's [Automata and Categories working group](https://autcat.github.io), a collaboration of the [Algebra and Computation](https://www.irif.fr/en/equipes/algebre/index) and [Automata](https://www.irif.fr/en/equipes/automates/index) teams of IRIF.
**References.** The list of references below is non-exhaustive, and is only included here to give an impression of some of the recent research that this project hopes to build on.
* [On duality and model theory for polyadic spaces](https://doi.org/10.1016/j.apal.2023.103388), Sam van Gool and Jérémie Marquès. Annals of Pure and Applied Logic 175, 2024.
* [Formalizing and computing propositional quantifiers](https://ipqcoq.github.io/cpp2023fereevangool-prepub.pdf), Sam van Gool and Hugo Férée. Certified proofs and programs (CPP), 2023.
* [Profinite lambda-terms and parametricity](https://entics.episciences.org/12280), Sam van Gool, Paul-André Melliès and Vincent Moreau. Mathematical Foundations of Programming Semantics (MFPS), 2023.
**Contact.** For more information about the project, please contact the project coordinator, Sam van Gool, .