جستجوی استاد راهنمای دانشگاهی

• Computational Complexity
• Geometry of Interaction
• Linear Logic
• +۴ مورد دیگر

Thomas Seiller is a CNRS researcher (Chargé de Recherche) working in the LoCal team at LIPN laboratory (Laboratoire d'Informatique de l'Université Sorbonne Paris Nord) and an associated researcher at IHPST (Institut d'Histoire et de Philosophie des Sciences et des Techniques). He serves as scientific secretary and board member of Section 06 (2021-2026) and as member of the Interdisciplinary committee CID 53 of the National Committee for Scientific Research (CoNRS). His PhD in mathematics from the Luminy Institute of Mathematics was supervised by Jean-Yves Girard and Laurent Regnier, focusing on Logic in the Hyperfinite Factor: Geometry of interaction and complexity . His research develops geometric approaches to computational complexity using dynamical systems and ergodic theory, building on Girard's geometry of interaction program through Interaction Graphs models of linear logic. Seiller leads multiple significant research projects including DySCo (Dynamical Systems and Computation), AlgoFormI (Algorithms: formalisation and impact), and FormA (Formalising algorithms). His work establishes connections between measurable group actions and complexity constraints, characterizing complexity classes through Interaction Graphs models. Scientific secretary of Section 06 (2021-2026) of CoNRS Principal Investigator for ANR JCJC project DySCo (258k€ funding) Organizer of major international workshops including Caleidoscope 2025 and Dagstuhl meetings He actively mentors PhD students including Yasmine Laghjichi (Models of computation), Eliès Harington (Higher-categorical polynomial models), Valentin Maestracci (proofs-as-programs interpretation), and Adrien Ragot (proof-nets). He organizes the 'Complexities' seminar and maintains public event calendars for his research community. His laboratory work centers on developing theoretical frameworks that connect dynamical systems to computational complexity while exploring formal definitions of algorithms across disciplines through projects like DySCo which aims to establish precise definitions of computation applicable across various computational models.

Georg Struthمشاهده پروفایل

استاد

• Logical and Algebraic Methods in Computer Science
• Formalised Mathematics
• Program Verification and Correctness
• +۷ مورد دیگر

Professor Georg Struth is a faculty member at the School of Computer Science , University of Sheffield. He serves as Head of the Foundations of Computation research group. Research Interests include logical and algebraic methods in computer science, formalised mathematics with interactive theorem provers, program verification, and hybrid systems. His work bridges foundational algebra (Kleene algebras, quantales, catoids) with practical verification tools in Isabelle/HOL. Recent Publications focus on higher-dimensional automata, modal algebras, and convolution-based concurrency models. Grants include EPSRC funding for hybrid system verification and concurrent algorithms. Teaching covers Hardware and Software Verification and formalised mathematics.

• Quantum Computing
• Quantum Mechanics
• Theoretical Computer Science
• +۳ مورد دیگر

Kang Feng Ng is a Research Fellow at the School of Electronic Engineering and Computer Science, Queen Mary University of London. His research focuses on foundational aspects of quantum computing and quantum mechanics, with a particular emphasis on diagrammatic calculi such as the ZX-calculus. His work explores completeness proofs for these frameworks and their applications to fermionic quantum systems and qubit-based quantum mechanics. Ng's research interests revolve around formalising quantum mechanics through diagrammatic methods, including axiomatisation of quantum circuits and analysis of computational completeness. He investigates how these mathematical tools can enhance understanding and design of quantum algorithms and systems. His publications emphasize theoretical advancements in quantum circuit models, with a recurring theme of extending and validating diagrammatic calculi for diverse quantum contexts. Despite no listed awards, his contributions highlight rigorous foundational work in quantum information theory. Ng has no recorded advisees or grants in the provided information. His affiliation with the School of Electronic Engineering and Computer Science positions him within a multidisciplinary environment focused on cutting-edge computing and engineering research.

Julien Narbouxمشاهده پروفایل

دانشیار

• Interactive Theorem Proving
• Formalization of Geometry
• Automated Reasoning in Geometry
• +۳ مورد دیگر

Julien Narboux is an Associate Professor (Maître de Conférence Hors Classe) at UFR Informatique, University Paris Cité, and a member of the PPS pole at the IRIF laboratory. He previously held the same position at the University of Strasbourg, affiliated with the ICube lab. His research focuses on interactive theorem proving, formalization of geometry, automated reasoning, and the use of proof assistants in education. Education: He earned his PhD in 2006 from Université Paris Sud-Paris XI, titled 'Formalisation et automatisation du raisonnement géométrique en Coq.' Research Interests : His work spans formal methods in geometry, development of proof assistants like Coq, and integrating these tools into education. Key areas include automated deduction in geometry, synthetic geometry formalization, and pedagogical applications of proof assistants. Recent Contributions : Recent work includes automated generation of illustrated proofs, constraint-solving approaches for theorem proving, and leveraging machine learning for geometry statement parsing. He actively contributes to projects like GeoCoq, formalizing high-school geometry problems. Grants & Projects : Leads the ANR APPAM project on proof assistants for mathematics education. Organized events include the 2023 ADG conference and ThEdu workshops. Advising : Supervised PhD students (e.g., Pierre Boutry) and master’s students in geometry formalization and related areas. Notable advisees include Frédéric Tran Minh and Salwa Tabet Gonzalez. Labs & Teams : Active in the IRIF lab and PPS team at University Paris Cité, collaborating on projects bridging formal methods and education.

Michael Norrishمشاهده پروفایل

دانشیار

• Formal Methods
• Interactive Theorem Proving
• Programming Languages
• +۴ مورد دیگر

Michael Norrish is an Associate Professor at the School of Computing, Australian National University (ANU) , specializing in formal methods, programming language semantics, and interactive theorem proving. His career spans roles at NICTA, Data61, and ANU, with a focus on mechanised mathematics and verified systems. PhD in Computer Science (University of Cambridge, 1999) Undergraduate degree from Victoria University of Wellington His research bridges interactive theorem-proving (ITP) systems like HOL4 with real-world systems verification, particularly in programming languages and compilers. He leads the CakeML project, developing a verified compiler for functional languages. His work intersects formal verification with practical system design, including projects on reproducibility debt in scientific software and verified processors. Recent publications highlight verified compilation techniques, reproducibility challenges, and Kolmogorov complexity formalization. He actively participates in conference program committees (e.g., CPP, PLDI) and promotes trustworthy systems development through tools like HOL4. Current affiliations: ANU, CakeML Project, Trustworthy Systems Research Group (UNSW) Collaborations: Chalmers University (postdoc opportunities), seL4 microkernel ecosystem