Andrej Bauer is a professor of computational mathematics at the Faculty of Mathematics and Physics, University of Ljubljana. His work spans foundations of mathematics, constructive and computable mathematics, type theory, homotopy type theory, and mathematical principles of programming languages. He is an author of the book “Homotopy Type Theory: Univalent Foundations of Mathematics” and the initiator of the HoTT library, an extensive formalization of homotopy type theory in the Coq proof assistant. He is also known for his seminal work with Matija Pretnar on programming with algebraic effects and handlers.
Matija Pretnar is an assistant professor of computational mathematics at the Faculty of Mathematics and Physics, University of Ljubljana. His research focuses on formalization, implementation, and semantics of programming languages. He is an expert on programming with computational effects, best known as the inventor (with Gordon Plotkin) of algebraic effect handlers.
Danel Ahman is a postdoctoral researcher and a teaching assistant at the Faculty of Mathematics and Physics, University of Ljubljana. His research focuses on programming language theory, and in particular topics in dependent and refinement types, the theory of computational effects, including categorical semantics, and the use of these for writing verified software.
Katja Berčič is a postdoctoral researcher and a teaching assistant at the Faculty of Mathematics and Physics, University of Ljubljana. She is interested in knowledge representation and management, particularly for mathematics. She is collaborating with KWARC on MathDataHub and building a bridge between a database of graphs and the Lean proof assistant together with Andrej Bauer and Jure Taslak.
Egbert Rijke is a postdoctoral researcher at the Faculty of Mathematics and Physics, University of Ljubljana. He is an expert on homotopy type theory and type-theoretic foundations of mathematics. He is currently writing a textbook on homotopy type theory.
Anja Petković Komel is a doctoral student at the Faculty of Mathematics and Physics, University of Ljubljana. In her dissertation she is studying meta-theoretic aspects of type theories, with an emphasis on type-theoretic transformations.
Jure Taslak is a doctoral student at the Faculty of Mathematics and Physics, University of Ljubljana. In his work he will investigate the interaction between formalized mathematics and databases of mathematical structures.