**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)** **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, .