Enrico Tassi is a researcher at Inria, France, affiliated with the STAMP team. His work focuses on the technology of formal proofs, particularly type theory, interactive theorem proving, and its application to formalizing mathematics. He is a key contributor to the development of tools like Coq-Elpi , Hierarchy-Builder , and the small scale reflection Coq extension. His research spans proof assistant architecture, software design, and formal verification, with a strong emphasis on free software principles. Enrico completed his Ph.D. at the University of Bologna in 2008, where he designed the Matita interactive theorem prover. He contributed to the formalization of the Odd Order Theorem and the Paral-ITP project, aiming to scale Coq for large mathematical libraries. His software projects include Elpi , a meta-language for proof assistants, and past contributions to Debian as a developer (2006–2016), focusing on integrating the Lua language into Debian systems. His publications highlight innovations in unification algorithms, tactical design, and proof structuring techniques. Articles address challenges in bi-directional type inference, pattern-based proof command focusing, and nonuniform coercion implementations. His work on small-scale reflection and Hierarchy-Builder demonstrates expertise in algebraic hierarchies and formal library management. Current efforts target enhancing OCaml-based systems through Elpi's high-level programming capabilities. Key Collaborations : Mathematical Components team (INRIA), D.A.M.A. Project Major Tools : Coq-Elpi, Hierarchy-Builder, Matita Formalization Efforts : Ordered Uniformities, Odd Order Theorem, Finite Group Theory
Sean Holden is a Professor in the Department of Computer Science and Technology at the University of Cambridge, affiliated with The Computer Laboratory. He holds positions at both the University and Trinity College. His research focuses on automated theorem proving, machine learning, and their intersections with formal methods and AI. He leads the development of the Connect++ theorem prover, which won the Best Newcomer award at CASC 2024. His work spans areas including connection calculus, graph neural networks, and reinforcement learning in games like Mahjong. Holden's academic contributions include over 50 publications in top venues such as IJCNN, ICPRAM, and Journal of Automated Reasoning. Notable works include foundational research on Bayesian methods in theorem proving and machine learning applications in bioinformatics and medical imaging. He serves as an Associate Editor for IEEE Transactions on Artificial Intelligence since 2023. His research group explores topics like protein graph embeddings, medical AI (e.g., breast cancer classification via MUGI-MRI), and the integration of machine learning with automated reasoning systems. Collaborations span institutions including Trinity College and international partners in computational biology and AI.
Jeremy Avigad is a Professor in the Department of Philosophy and the Department of Mathematical Sciences at Carnegie Mellon University, where he serves as Director of the Hoskinson Center for Formal Mathematics and holds a Dean's Chair in Logic and Philosophy of Mathematics. His primary research interests include Formal Methods and AI for mathematics, mathematical logic, and the history and philosophy of mathematics. His work bridges deep theoretical inquiry with practical applications, particularly in formal verification and automated reasoning. His recent publications reflect a strong focus on the formalization of mathematics, automated reasoning, and the integration of AI techniques into theorem proving. Key themes include the development and application of the Lean theorem prover, premise selection, proof optimization, and the formal verification of computational claims, especially in the context of blockchain technology. CADE-25 Skolem Award Avigad advises PhD students, such as Chase Norman, and is involved in significant research grants and collaborations, including work with StarkWare. He is an active organizer of major academic events like Big Proof and the Formalization of Mathematics workshops. He leads the Hoskinson Center for Formal Mathematics, a research hub dedicated to advancing the field of formal mathematics.
Amey Bhangale is an Assistant Professor in the Department of Computer Science and Engineering at the University of California, Riverside. Prior to this, he held positions as a post-doctoral fellow at the Weizmann Institute of Science under Irit Dinur and a research fellowship at the Simons Institute. His research focuses on Approximation Algorithms , Probabilistically Checkable Proofs , Hardness of Approximation , and Analysis of Boolean Functions . Research Trends His recent work explores inapproximability bounds for constraint satisfaction problems, parallel repetition theorems, and additive combinatorics in finite fields. Notable collaborations include Subhash Khot, Dor Minzer, and Yang P. Liu. Teaching CS219: Advanced Algorithms (2025) CS141: Intermediate Data Structures and Algorithms (2024) CS218: Design and Analysis of Algorithms (2023) CS215: Theory of Computations (2021-2023)
Alessandro Artale is an Associate Professor in the Faculty of Computer Science at the Free University of Bozen-Bolzano, where he is affiliated with the KRDB Research Centre. His research spans theoretical and applied aspects of knowledge representation, ontologies, and temporal reasoning. He earned his PhD in Computer Science from the University of Florence in 1994 and has held research and academic positions at CNR-LADSEB, IRST (now FBK), and UMIST (University of Manchester). PhD in Computer Science, University of Florence, 1994 His research interests include: Description Logics Ontologies and Conceptual Modelling Temporal and Computational Logics Knowledge Representation and Databases Artificial Intelligence and Natural Language Semantics His recent scholarly activities are reflected in his participation in leading international conferences such as AAAI, IJCAI, ECAI, KR, DL, TIME, and FoIKS. These publications and committee roles highlight a consistent focus on formal methods in AI, particularly in the areas of description logics, temporal reasoning, and ontology-based systems. The research demonstrates a strong theoretical foundation with applications in semantic web technologies and knowledge-driven systems. Notable scientific contributions include: Principal Investigator of the EPSRC project on Temporal Databases using Description Logics (2001–2004) Member of the KnowledgeWeb Network of Excellence Member of the InterOp Network of Excellence Member of the ESPRIT DWQ project on Data Warehouse Quality Artale has advised numerous Master's and PhD students through project supervision and has organized academic events such as the TIME and DL workshops. He has served on the program committees of over 50 international conferences and workshops, demonstrating extensive engagement with the research community. His teaching includes core computer science courses in algorithms, formal languages, compilers, and discrete mathematics. He is actively involved in research labs and teams including: KRDB Research Centre, Free University of Bozen-Bolzano Collaborations with European research networks (KnowledgeWeb, InterOp)
Bruno Lopes is a Professor at Universidade Federal Fluminense (UFF) and a researcher at the FR∀M∃ Lab. He holds a D.Sc. in Informatics (Theory of Computation) from PUC-Rio and has conducted postdoctoral work at INRIA (France). His academic roles include serving on the Brazilian Logic Society's directive committee (SBL) from 2017-2019, 2019-2021, and 2023-2025, and as 2nd Vice-President of SBL. He also coordinated the Logic Interest Group at the Brazilian Computer Society (SBC, 2020-2024). Research focuses on formal methods, logic systems, and theorem proving. Notable areas include proof theory, modal logics, concurrent systems, and multi-agent systems formalization. His work intersects theoretical foundations with applied domains like extensible theorem provers and ontology development. Education: D.Sc. in Informatics (PUC-Rio), M.Sc. in Geostatistics (UFAL), B.Sc. in Computer Science (UFAL). Teaches courses such as Logic and Formal Methods (TCC00305), Logic Programming (TCC00304), and Programming I (TCC00308). Active in international collaborations with INRIA and Université Lyon 3. Advances formal methods through projects like the TecMF/PUC-Rio initiative. His research emphasizes logical frameworks for concurrent systems and extensible theorem proving tools.
Professor Zhengfeng Ji is an Adjunct Professor at the Centre for Quantum Software and Information within the Faculty of Engineering and Information Technology at the University of Technology Sydney. His research focuses on quantum computation, quantum information theory, and quantum communication. Quantum complexity theory Quantum algorithms Quantum network optimization Entanglement characterization Recent publications highlight advancements in quantum network routing frameworks and quantum proof systems. He has secured multiple grants including the Sydney Quantum Academy Postdoctoral Fellowship and ARC Discovery Projects. Quantum Exponential Time Hypothesis Quantum PCP Conjecture Post-quantum Cryptographic Protocols Scientific awards include: SQA Scholarship Sydney Quantum Academy Postdoctoral Fellowship SUSTech Scholarship
Dr. Kim Völlinger is a Researcher at the Technical University of Berlin in the Models and Theory of Distributed Systems group. Her academic career spans formal methods, trustworthy machine learning, and distributed systems, with a focus on integrating interactive proof assistants like Coq for neural network verification. Education: Computer Science with a minor in Cognitive Psychology at Humboldt University of Berlin and ENSEEIHT in Toulouse, France PhD Supervisors: Wolfgang Reisig (HU Berlin), Kurt Mehlhorn (MPI-INF Saarbrücken), Holger Schlingloff (Fraunhofer FOKUS) Her research bridges theoretical computer science and practical verification, exploring witness-based runtime verification for asynchronous systems, hybrid system formalization, and LLM-supported proof synthesis. She also contributes to interdisciplinary collaborations, particularly evident in her microbiology-related publications. Recent publications on Google Scholar highlight her work in environmental microbiology, including microbial community dynamics in petroleum reservoirs, DNA extraction from crude oil, and bacterial stress responses in extreme saline environments. These studies reflect cross-disciplinary applications of computational modeling to environmental systems. Teaching activities include formal languages, automata theory, and interactive theorem provers. She actively mentors doctoral students, leads research-oriented master's projects, and supervises student theses. The Models and Theory of Distributed Systems group at TU Berlin serves as her primary research environment, where she continues to develop tools for computational verification and machine-reviewed proofs.
Magnus O. Myreen is a Professor in the Department of Computer Science and Engineering at Chalmers University of Technology, Sweden. He has been with Chalmers since 2014, becoming a tenured Associate Professor in 2015 and being promoted to full Professor in June 2023. Myreen has an extensive record of service to the programming languages and formal methods communities, including serving on program committees for major conferences like PLDI, POPL, ICFP, and CPP, and chairing the steering committee for the ITP conference series since November 2023. Myreen received his academic training at prestigious institutions: B.A. in Computer Science at the University of Oxford, tutored by Dr. Jeff Sanders Ph.D. on program verification in 2009 at the University of Cambridge, supervised by Prof. Mike Gordon Myreen's research focuses on program verification, interactive theorem proving, and compiler verification. He is best known for his work on the CakeML project, which is an ML-style language with a formal semantics and a growing ecosystem of proofs and tools that support construction of verified applications. As he states on his website, "My most recent work has focused on CakeML, which is an ML-style language with a formal semantics and a growing ecosystem of proofs and tools that support construction of verified applications. As far as I know, the CakeML compiler is the first verified compiler to have been bootstrapped." His research spans several key areas: Decompilation into logic — verification of machine code Proof-producing synthesis from logic Verified Lisp and ML runtimes Connecting things up: verified stacks Myreen's publication record shows a strong focus on verified compilation and theorem proving, particularly through the CakeML ecosystem. His work consistently bridges the gap between theoretical foundations and practical implementation, with numerous papers on verified compilers, program verification, and theorem proving. A significant trend in his recent work (2021-2024) has been extending CakeML's capabilities to handle more complex language features, improve performance, and verify increasingly sophisticated compilation techniques including bootstrapping and dynamic computation. Myreen has received several prestigious awards and recognitions: Winner of the BCS Distinguished Dissertation Competition 2010 for his PhD work Royal Society Research Fellow (UK) since 2012 ACM SIGPLAN Most Influential POPL Paper Award for the 2014 CakeML paper Amazon Research Award for his proposal "Compiling Dafny to CakeML" Myreen has advised several PhD students to completion, including Alejandro Gomez (Sep 2017 – Jun 2023), Oskar Abrahamsson (Aug 2017 – Dec 2022), and Andreas Loow (Sept 2016 – Sep 2021). He also collaborated with postdocs including Hira Syeda, Thomas Sewell, and Johannes Aman Pohjola. His research has been supported by various funding sources, though specific grants aren't detailed in the provided text. Notably, he received an Amazon Research Award for his work on compiling Dafny to CakeML, and his CakeML project has clearly attracted significant attention in the programming languages and formal methods communities. Myreen leads research on the CakeML project, which has grown into a substantial ecosystem for verified compilation. The project involves a team of researchers working on various aspects including compiler verification, program synthesis, and theorem proving. Myreen also collaborates with researchers at other institutions, as evidenced by his visits to EPFL (meeting Viktor Kuncak, Martin Odersky, and James Larus) and NUS (visiting Ilya Sergey's group). In October 2023, he began a ten-month sabbatical at Cambridge UK, where he worked part-time for Arm Ltd., indicating ongoing industrial collaboration.
Ilya Sergey is an Associate Professor at the National University of Singapore (NUS) School of Computing, with previous faculty appointments at University College London (2015-2018). His academic career spans multiple prestigious institutions including IMDEA Software Institute (postdoctoral position) and KU Leuven (PhD). His educational background includes a PhD in Computer Science from KU Leuven (2012), an MSc in Mathematics and Computer Science from Saint Petersburg State University (2008), and professional experience as a software engineer at JetBrains prior to academia. Sergey's research focuses on the intersection of programming language theory and practical software verification, with particular emphasis on concurrent systems , smart contracts , and program synthesis . His work bridges theoretical foundations in type theory and separation logic with practical applications in blockchain technology and Rust programming. He has developed novel techniques for verifying heap-manipulating programs, analyzing commutativity in distributed transactions, and synthesizing correct-by-construction code. Analysis of his recent publications reveals a clear trajectory toward practical verification of blockchain systems and concurrent data structures, with increasing focus on Rust programming language applications. His work demonstrates consistent innovation in mechanized reasoning techniques while maintaining relevance to real-world software challenges, particularly in the domains of smart contracts and distributed systems. Sergey maintains an active research group at NUS, as evidenced by his social media references to lab traditions and student collaborations. He frequently participates in major programming languages conferences as both author and committee member, serving in leadership roles including General Chair for ICFP 2025. His research lab follows distinctive traditions, including location-based Mattermost status updates when traveling. Sergey is deeply engaged with the programming languages community through conference organization, mentoring activities, and outreach initiatives such as nature walks for conference attendees.
Panagiotis (Pete) Manolios is a Professor in the Department of Computer Science within Northeastern University's College of Engineering in Boston. He leads the Northeastern University Formal Methods (NUFM) research group and maintains an active research program with multiple current PhD students. His primary affiliation is with the College of Computer Science (CCS) at Northeastern University, where he holds a tenured faculty position. Manolios' research focuses on formal methods with particular emphasis on program verification, theorem proving, and safety analysis of systems. His work spans several key areas including floating-point program analysis, resource-aware program verification, protocol verification, and safety-critical systems. He has developed significant tools and methodologies such as ACL2s (a powerful theorem prover) and pioneered approaches for analyzing numeric stability in compiler optimizations. His recent publications demonstrate substantial activity in formal verification, with particular focus on numeric stability analysis, invariant discovery through gamification, and model-based safety analysis of complex system architectures. These works reflect a consistent research trajectory toward making formal verification more practical and applicable to real-world systems, especially those with safety-critical requirements. Manolios has received recognition through multiple NSF grants including the SaTC: CORE: Medium collaborative project on bridging the gap between protocol design and implementation. His work on confidentiality and integrity of deep neural networks represents cutting-edge research at the intersection of formal methods and AI security. He has successfully mentored numerous PhD students who have gone on to positions at major technology companies including Google, Facebook, Intel, and MathWorks. His students' dissertations cover diverse topics within formal methods, from rank-polymorphic programming languages to resource-aware program analysis. Manolios directs several significant research projects including ACL2s (a powerful theorem prover), CID: Confidentiality and Integrity of Deep Neural Networks, Compilation-Dependent Security Properties of Software, and Platform Dependencies of Floating-Point Programs. These projects address fundamental challenges in making formal verification more practical and applicable to real-world systems.
