Justin Thaler is an Associate Professor in the Department of Computer Science at Georgetown University, researching algorithms and computational complexity with focus on probabilistic proof systems, verifiable computation, and streaming algorithms. Education: PhD Computer Science, Harvard University BS Computer Science and Mathematics, Yale University Research Interests: Develops protocols for verifying computations (including zero-knowledge proofs), analyzes the power of low-degree polynomials, and designs efficient streaming/sketching algorithms for large datasets. Publications: Research advances theoretical foundations of proof systems, with recent work on SNARKs, lookup arguments, and Fiat-Shamir security. Authored the monograph 'Proofs, Arguments, and Zero-Knowledge'. Advising & Labs: Advises PhD students in theoretical computer science. Contributes to open-source projects including DataSketches library of streaming algorithms. Currently on leave at a16z crypto research.
Prof. Christoph Benzmüller is a Full Professor at the University of Bamberg (Chair for AI Systems Engineering) and an adjunct professor at Freie Universität Berlin's Department of Mathematics and Computer Science. He is a leading researcher in automated reasoning, computational metaphysics, and formal logic systems. His work focuses on integrating higher-order logic into AI to achieve transparent and ethically grounded systems. Research Interests: His research spans automated theorem proving, formal ontologies, and normative reasoning in AI. Notably, he has formalized Gödel's ontological argument using computational methods and developed the Leo theorem provers for higher-order logic. He emphasizes the use of symbolic reasoning for ethical and legal AI frameworks. Grants & Projects: He leads projects like PetraKIP (AI portfolios for teacher education) and NFDIxCS (National Research Data Infrastructure). His work is funded by DFG, EPSRC, and the Volkswagen Foundation. He also collaborates with institutions globally, including Stanford and Cambridge. Awards: Recipient of the Central Teaching Award (FU Berlin) for his Computational Metaphysics course and a DFG Heisenberg Fellowship. His research on Gödel's argument gained international media attention. Education: Studied at Saarland University, where he earned his PhD (1999) and habilitation (2006).曾是专业长跑运动员，后转向学术研究。
Dr. Athina Thoma is a Lecturer in Mathematics Education within the Southampton Education School at the University of Southampton. Her research focuses on university-level mathematics education, including the transition from secondary to tertiary mathematics, the role of programming in undergraduate learning, and students' proof production using interactive theorem provers. Research Interests: Teaching and learning methodologies in university mathematics Educational transitions between secondary and higher education Integration of computational tools (e.g., programming) in mathematics education Students' engagement with formal proof construction Dr. Thoma is currently accepting applications for PhD supervision. No specific grants, labs, or awards are listed in the provided profile.
Théo Winterhalter is a researcher at INRIA Saclay and a member of the Laboratory of Mathematics and Computer Science (LMF) at ENS Paris-Saclay . He previously held a postdoctoral position at the Max Planck Institute for Security and Privacy (MPI-SP) and completed his PhD at the Gallinette research team in Nantes, supervised by Nicolas Tabareau and Matthieu Sozeau. Education PhD in Computer Science, 2017–2020, University of Nantes (Gallinette/Inria) MSc in Computer Science, École Normale Supérieure de Rennes Research interests include type theory , proof assistants , formal verification , and dependent types . He actively works on improving the safety and usability of proof assistants like Rocq (formerly Coq), focusing on rewrite rules, erasure, and cryptographic verification. His work often involves formalizing results within proof assistants and developing tools for verified programming. Contributions span conferences like POPL, ICFP, CPP, and TYPES. Recent projects include foundational verification of high-speed cryptography ( The Last Yard ), type-preserving rewrite rules ( The Rewster ), and modular cryptographic proofs ( SSProve ). His publications emphasize formal methods and computational assumptions in type theory. Teaching includes the Proof Assistants course at MPRI , a joint master’s program. He co-supervises PhD students like Yann Leray and has mentored interns on topics such as erased data implementation and Autosubst tooling. Labs and Teams : Deducteam (INRIA Saclay) – Developing deduction tools and formal verification LMF (ENS Paris-Saclay) – Laboratory for Mathematics and Computer Science Gallinette (former) – Team at INRIA Nantes MetaCoq Project – Collaborative effort on Coq verification
John Wright is an Assistant Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. His research centers on theoretical computer science with a focus on quantum computing, specifically quantum state learning, quantum complexity theory, property testing, and approximation algorithms. He is affiliated with the Simons Institute for the Theory of Computing. Education includes a Ph.D. in Computer Science from Carnegie Mellon University (2016), advised by Ryan O'Donnell, and a B.Sc. in Computer Science from the University of Texas at Austin. Research interests span quantum complexity, interactive proofs (e.g., MIP* = RE), quantum algorithms, and foundational aspects of quantum computation. His work bridges computer science, physics, and mathematics, with emphasis on understanding computational limits through quantum paradigms. Publications primarily explore quantum complexity, algorithms, and verification, with recent trends including quantum cryptography, tomography, and hardness proofs. Articles frequently involve collaborations with researchers like Thomas Vidick, Henry Yuen, and Ryan O'Donnell. Awards include the IEEE CS TCPAMI Young Researcher Award (2015). Teaching covers graduate and undergraduate courses such as CS 170 (Efficient Algorithms and Intractable Problems) and CS 294 (Quantum Complexity Theory). He advises students in quantum computing research and collaborates extensively across institutions. Labs/teams include the Quantum Computing group at UC Berkeley, with ties to the Simons Institute. Research support is managed by Amy Frithsen.
Jasmin Blanchette is a Professor of Theoretical Computer Science and Theorem Proving at the Institute for Informatics, Ludwig-Maximilians-Universität München (LMU), where he also serves as Dean of Studies for Computer Science since January 2024. He is additionally affiliated as a guest researcher with the VeriDis group at Loria in Nancy, France. His research lies at the intersection of automated and interactive theorem proving, with a focus on higher-order logic and proof automation. Key projects include the development of tools like Sledgehammer, Nitpick, and Zipperposition, and foundational work on (co)datatypes and higher-order superposition. His recent publications reflect a strong trend in formalizing and verifying automated reasoning techniques, especially in higher-order logic, with applications in proof automation, SMT solving, and logical verification. Articles frequently appear in top venues such as CADE, ITP, and the Journal of Automated Reasoning. CADE 2023 Best Paper Award for 'Verified given clause procedures' FroCoS 2023 Best Paper Award (with Visa Nummelin and Sander Dahmen) IPA Dissertation Award (awarded to his student Petar Vukmirović) Dutch 'cum laude' distinction (awarded to his student Anne Baanen) Dutch Prize for ICT Research 2022 Blanchette has advised numerous PhD and postdoctoral researchers, many of whom are now active contributors to the formal methods community. He has received significant research grants through projects like Matryoshka and Nekoka. He is also the editor-in-chief of the Journal of Automated Reasoning and plays a central role in organizing key conferences such as ITP, CADE, and CPP. He leads an active research group at LMU, consisting of postdocs and PhD students working on topics such as higher-order superposition, formalization of voting systems, categorical logic, and proof search heuristics. The team collaborates closely with international groups, including those at Inria and TU Wien.
Yupeng Zhang is an Assistant Professor at the University of Illinois Urbana-Champaign in the Department of Electrical and Computer Engineering, with an affiliate appointment in Computer Science. His research focuses on cybersecurity and applied cryptography , particularly zero-knowledge proofs , secure multiparty computations , and their applications in blockchain and machine learning. Education: Ph.D., Electrical and Computer Engineering, University of Maryland (2018) M.Phil., Information Engineering, Chinese University of Hong Kong (2013) Bachelor of Engineering, Information Engineering, Chinese University of Hong Kong (2011) Research Highlights: Developed scalable zero-knowledge proof systems for blockchain and machine learning Created verifiable computation frameworks for SQL and RAM Advancing privacy-preserving ML and cross-chain blockchain bridges Grants: NSF CAREER award Air Force Research Lab DARPA Google Research Scholar Award Facebook Research Award Latticex Foundation Teaching: CS 461/ECE 422: Computer Security I CS 591 SP: Security and Privacy ECE 407/CS 407: Cryptography ECE 598 YPZ: Advanced Topics in Applied Cryptography Co-taught MOOC on Zero-Knowledge Proofs (Spring 2023) Professional Service: Program Vice Co-Chair, USENIX Security 2024 Program Committee, Crypto 2025, S&P 2025 Reviewer for major journals and conferences
Frédéric Tran Minh is a Lecturer at Esisar – Grenoble INP-UGA and a PhD student affiliated with the CTSYS team at LCIS laboratory. His career spans academic teaching, software development, and research in formal verification for education. PhD in progress on proof assistants for teaching mathematics Former software engineer in computer-assisted surgery (8 years) Member of the APPAM ANR project Develops the Yalep proof assistant environment Research focus: Integration of Lean theorem prover and mechanized proofs into undergraduate mathematics pedagogy, emphasizing interactive learning and web-based accessibility. Teaching areas: Algebra, Analysis, C Programming, and automata theory, with innovative use of proof assistants in curricula.
Emily First is an incoming Assistant Professor in Computer Science at Rutgers University New Brunswick starting Fall 2025. She previously served as a postdoctoral researcher at UC San Diego under Sorin Lerner and earned her PhD in Computer Science at UMass Amherst under Yuriy Brun in the Laboratory for Software Engineering Research (LASER). Her research focuses on leveraging AI for theorem proving, working at the intersection of machine learning, software engineering, and programming languages. She specializes in creating tools for automated proof generation in proof assistants like Coq, Isabelle/HOL, and Lean. Her work explores how AI can enhance human reasoning across domains, with applications in software verification and formal logic systems. Recent publications show trends in neuro-symbolic AI, software verification, and LLM integration for formal methods. Her team's research has been recognized with ACM SIGSOFT Distinguished Paper Awards at ICSE, ACL, and ESEC/FSE conferences, along with workshop presentations at AI and Theorem Proving conferences. ACM SIGSOFT Distinguished Paper Award (ICSE 2025) ACM SIGSOFT Distinguished Paper Award (ACL Main 2024) ACM SIGSOFT Distinguished Paper Award (ESEC/FSE 2023) ACM SIGSOFT Distinguished Paper Award (ICSE 2022) Contact: emfirst@ucsd.edu (new email coming soon).
Kevin Buzzard is a Professor of Pure Mathematics at the Department of Mathematics, Faculty of Natural Sciences, Imperial College London. His work focuses on formal proof verification and the integration of computers into mathematical research. He leads projects formalizing mathematical theorems using Lean, including a 21st-century proof of Fermat’s Last Theorem. Notable talks include the 2024 Stanford MRC Public Lecture on AI in mathematics and the 2022 International Congress of Mathematicians plenary lecture on formalism trends. His research spans Pure Mathematics and Computation Theory, emphasizing collaboration between mathematicians and computer scientists. He co-maintains Mathlib, a formalized mathematical library, and teaches Lean to undergraduates. Awards include the Whitehead Prize (2023) and Senior Berwick Prize (2023) from the London Mathematical Society. Buzzard’s career includes research positions at the University of Cambridge, Harvard, and the Institute for Advanced Study. He explores how AI and theorem provers will transform mathematical practice, advocating for formalization as a foundational tool for future mathematics.
Hamed Nemati is an Assistant Professor at the Division of Network and Systems Engineering under the School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology in Stockholm, Sweden. He was previously a Visiting Assistant Professor at Stanford University and a Research Group Leader at the Helmholtz Center for Information Security (CISPA) , where he also worked as a PostDoc and Research Fellow. Education : PhD in Computer Science from KTH Royal Institute of Technology Research Interests : Security of systems software, formal methods and program logics, interactive theorem proving, machine code analysis, applied machine learning Current Projects : Systematic verification of multi-language security protocols, hardware-software co-design for Spectre mitigation, capability-based access control models Scientific Awards : WASP (Wallenberg AI, Autonomous Systems and Software Program) faculty member Teaching Activities : Formal Methods in Security (Fall 2020-2023) at CISPA/Saarland University Digital Forensics and Incident Response (EP2780) (Fall 2024) at KTH
Robert Y. Lewis is a Lecturer in the Department of Computer Science at Brown University, specializing in formal methods, logic, and interactive theorem proving. His work bridges computer science and mathematics, focusing on the verification of mathematical proofs and program correctness. Education: PhD in Pure and Applied Logic (2018), Carnegie Mellon University MS in Pure and Applied Logic (2015), Carnegie Mellon University BA in Mathematics (2010), Rice University Research Interests: Lewis’s research spans formal verification, logic, type theory, and automated reasoning. He explores the application of logical tools like the Lean proof assistant in mathematics education and software verification. Teaching: At Brown, he teaches courses such as Introduction to Discrete Structures and Probability and Formal Proof and Verification . Prior to Brown, he taught Logic and Modeling at Vrije Universiteit Amsterdam and served as a teaching assistant at Carnegie Mellon University. Publications: His recent work includes advancements in formalizing mathematical structures (e.g., Witt vectors, Cap Set Problem), integrating proof assistants with computational tools (Lean-Mathematica interface), and developing educational resources for logic and formal methods. Contact: Email: robert_lewis@brown.edu Office: Center for Information Technology 203, Brown University
Clément Pit-Claudel is an Assistant Professor at École Polytechnique Fédérale de Lausanne (EPFL), leading the SYSTEMF lab focused on programming languages, formal methods, and systems engineering. His work bridges mathematical formalisms with practical system development to achieve full assurance in critical software and hardware. PhD in Computer Science from MIT (2016) William A. Martin Memorial Thesis Award recipient Former Senior Applied Scientist at Amazon AWS Teaching accolades including the Frederick C. Hennie III Teaching Award Research spans three axes: extensible proof-producing compilers for performance-critical systems, verified hardware compilation with cycle-accurate semantics, and interactive theorem prover tooling for democratizing verification technology. Key projects include Kôika for hardware verification, Alectryon for Coq proof visualization, and Fiat for correct-by-construction program synthesis. Recent publications address JavaScript regex verification (ICFP 2024), cryptographic server integration (PLDI 2024), and hardware simulation optimization (ASPLOS 2021). Articles demonstrate expertise in functional-to-imperative translation, domain-specific compiler extensions, and hardware-software co-verification. Scientific contributions recognized through: Distinguished artifact award (SLE 2020) MIT William A. Martin Thesis Award Frederick C. Hennie III Teaching Award Teaching philosophy emphasizes hands-on lab instruction , oral assessment , and automated tooling . Courses taught include Software Construction (undergraduate) and Interactive Theorem Proving (graduate) at EPFL. Research service includes program committee roles at Dafny, POPL, and SPLASH conferences.
Dr. Heather Macbeth is a Senior Lecturer in Pure Mathematics at Imperial College London, specializing in Kähler geometry, geometric analysis, and the formalization of mathematics. Her research develops geometric analysis techniques for complex manifolds while advancing proof verification through the Lean theorem prover. She leads the development of Lean's Mathlib library, creating formalizations for differential geometry, functional analysis, and representation theory. Her textbook The Mechanics of Proof introduces proof writing through Lean, integrating computer verification with mathematical pedagogy. Funded by a Microsoft Research Lean Award, Dr. Macbeth organizes workshops on formal mathematics and serves on the AMS Committee on Publications. Her geometric research examines Ricci solitons, Yamabe invariants, and Kähler-Einstein metrics, while her formalization work includes Sobolev inequalities and semilinear functional analysis. Research Contributions: Geometric analysis of Ricci solitons and Kähler metrics Formal verification of functional analysis theorems Proof assistant pedagogy and textbook development Contributions to Lean's mathematical library
Asta Halkjær From is a postdoctoral researcher in the Department of Computer Science at the University of Copenhagen, affiliated with the Software, Data, People & Society (SDPS) section under Dmitriy Traytel. She previously completed her PhD at DTU Compute from 2020 to 2023, focusing on formalized deduction methods in computational logic. She holds a Master’s and Bachelor’s degree from DTU in Computer Science and Software Technology, respectively, with a specialization in Artificial Intelligence and Algorithms. Her research lies at the intersection of formal logic and computer science, particularly in automated reasoning, proof assistants (Isabelle/HOL and Lean), and mechanized metatheory. She has contributed extensively to synthetic completeness proofs, tableau systems, and verified theorem provers. Her work emphasizes formal verification of logical systems, including epistemic logic, hybrid logic, and first-order logic, with a focus on soundness and completeness. The recent publications highlight a consistent trend: the mechanization of logical foundations in proof assistants. Her work bridges theoretical logic with practical verification tools, enabling reliable automation in theorem proving. She has developed and verified provers, explored axiomatic systems, and advanced the methodology of synthetic completeness, often leveraging Isabelle/HOL’s framework. Distinguished Paper Award, CPP 2023 DTU Young Researcher Award DTU Travel Grant (Executive Board Recognition) Otto Mønsted Fonden Travel Grant She has supervised BSc and MSc theses, special courses, and research projects at DTU, and currently teaches Software Development for Digital Health . She has served on program committees for CPP, ITP, and Dalí workshops and has reviewed for journals including Journal of Automated Reasoning and Journal of Logic and Computation . She has also participated in international research visits, including at VU Amsterdam. She is actively involved in building tools for formal reasoning and maintains a personal website with resources, including an Isabelle snippets generator and bibliography tools. Her work continues to advance the foundations of formal logic through mechanized proofs and practical automation.
