Neelakantan R. Krishnaswami is a Professor of Computer Science at the University of Cambridge's Computer Laboratory , and a Fellow of Trinity College . His research focuses on the intersection of program verification, programming language design, and foundational topics like type theory and semantics. His work spans areas such as refinement types, parser design, separation logic for systems software, and the semantics of reactive programming. Notable contributions include the Datafun language for higher-order Datalog and the λert type theory for explicit refinement types. He has also developed foundational frameworks for verifying imperative programs using advanced type systems and logical relations. Key publications include 'Explicit Refinement Types' (ICFP 2023), 'flap: A Deterministic Parser with Fused Lexing' (PLDI 2023), and 'CN: Verifying Systems C Code' (POPL 2023). His work frequently addresses challenges in efficiency, correctness, and modularity for both functional and imperative systems. His awards include Distinguished Paper Awards at PLDI 2019 and POPL 2020. His research integrates theoretical rigor with practical tooling, exemplified by contributions to languages like Coq, Lean, and Haskell.
Daniel M. Roy is a Professor at the University of Toronto with cross-appointments in the Departments of Computer Science and Electrical and Computer Engineering. He serves as Associate Chair, Statistics, and is a Research Director at the Vector Institute and a CIFAR Canada AI Chair. His research focuses on foundational principles of prediction, inference, and decision-making under uncertainty, spanning machine learning, statistics, mathematical logic, applied probability, and computer science. He has contributed to learning theory, statistical network analysis, probabilistic programming, and Bayesian nonparametric statistics. Education: Ph.D. in Computer Science from MIT (2011), advised by Leslie Kaelbling. Postdoctoral fellowships at the University of Cambridge (Newton International Fellow and Research Fellow). His research explores information theories of learning , online learning , and nonstandard foundations for decision theory . Recent work includes best paper awards at ICML 2024 and advancements in probabilistic programming systems like Church. His publications address problems in generalization bounds, causal bandits, neural network theory, and exchangeable random structures. Scientific Awards include the MIT/EECS George M. Sprowls Doctoral Dissertation Award and the ICML 2024 Best Paper Award. He advises students and postdocs across statistics, computer science, and machine learning, with alumni now holding positions at institutions like Princeton, Imperial College London, and the University of Chicago.
Stefano Gogioso is a Departmental Lecturer at the University of Oxford , specializing in quantum theory and quantum software. He holds a DPhil in Computer Science from Oxford (2013–2017) and advanced degrees from Cambridge (MASt, BA) and the University of Genova (MSc, BSc). As a Fellow at Kellogg College and co-founder of Hashberg Ltd , he develops quantum programming tools and focuses on quantum causal structures, quantum field theory, and natural language processing applications. His research bridges foundational quantum theory with practical applications, including near-term quantum computing and educational outreach through visual methods like Quantum in Pictures . Research Interests: Quantum foundations, quantum software, categorical quantum mechanics, quantum field theory, and quantum causality. His work emphasizes pictorial formalisms and compositional methods, with contributions to indefinite causality, quantum cellular automata, and quantum natural language processing (QNLP). Key Contributions: Published over 25 papers, including works on causal polytopes, categorical Feynman diagrams, and QNLP pipelines. Co-developed Hashberg 's quantum programming tools and serves as a mentor for AI initiatives at CDL-Oxford. His thesis introduced dynamics in categorical quantum mechanics, addressing symmetry and quantum clocks. Teaching: Teaches quantum computing courses for MSc/MFoCS students, professionals, and continued education. Courses include Quantum Software , Quantum Computing for Software Engineers , and bespoke corporate training. Labs/Teams: Part of the Oxford Quantum Group and involved in collaborative projects with industry and academia. Advising: Supervised students like Nicola Pinzani (causal orders) and Maria Stasinou (quantum field theory). Grants/Awards: Not explicitly listed, but recognized for contributions to quantum foundations and education.
Ernest Davis is a Professor at the Department of Computer Science , Courant Institute of Mathematical Sciences , New York University . His research focuses on representing commonsense knowledge in AI systems , with an emphasis on spatial and physical reasoning , and he collaborates with Gary Marcus on integrating AI and psychological models. He has authored over 50 scientific papers and three books, including Linear Algebra and Probability for Computer Science Applications (2012). His teaching includes courses on Artificial Intelligence and Fundamental Algorithms. Research Trends: His recent work examines benchmarks for commonsense reasoning , limitations of large language models (e.g., GPT-4, DALL-E 2), mathematical reasoning in AI, and the Winograd Schema Challenge . Professional Activities: He has served as an ACM reviewer, program committee member for 50+ conferences, and area editor for ACM Transactions on Computational Logic . He contributes book reviews to Computing Reviews , SIAM News , Artificial Intelligence journal, and others. Non-Technical Writing: Davis writes for general audiences on topics spanning computer science, mathematics, cognitive psychology, and literary themes, published in outlets like The New Yorker , Wired , and The Times Literary Supplement .
Pavel Panchekha is an Assistant Professor in the School of Computing at the University of Utah, where he holds the Warnock Chair for Junior Faculty. His research spans programming languages, web browsers, and numerical analysis, with a focus on developing programming language techniques to address challenges across computer science. Dr. Panchekha received his educational training at prestigious institutions: PhD in Computer Science from the Paul G. Allen School for Computer Science and Engineering at the University of Washington, advised by Michael D. Ernst and Zachary Tatlock BS in Mathematics from MIT Panchekha's research program has two major thrusts. First, he works on web browser internals , with projects including fuzzing layout invalidation, multi-tenant garbage collection, and optimizing 2D graphics. He is also authoring a textbook on web browsers that informs much of this research. Second, he focuses on automatic numerical analysis , with projects such as automatic accuracy improvement, synthesis via term rewriting, scalable static accuracy analysis, and math library implementation. He leads the FPBench and Herbie projects, which are major deployments of his research. His scholarly output demonstrates consistent contributions across programming languages, verification, and numerical methods. Recent work shows a growing emphasis on bidirectional typing systems, layout invalidation in browsers, and robust floating-point error analysis. His publications reveal a trajectory from foundational work on floating-point accuracy (notably the Herbie tool that won a Distinguished Paper Award at PLDI 2015) toward more comprehensive systems for program synthesis, verification, and browser optimization. Panchekha has received significant recognition for his research contributions: NSF Fellowship ARCS Foundation Fellowship Adobe Research Fellowship Wissner-Slivka Foundation Fellowship 2015 PLDI Distinguished Paper Award for work on the Herbie numerical analysis and repair tool As an advisor, Panchekha mentors a substantial group of students across multiple levels. He currently advises six students: Marisa Kirisame (PhD), Bhargav Kulkarni (PhD), Yumeng He (PhD), Artem Yadrov (MS), Jesus Ponce (BS), and Jonas Regehr (BS). Previously, he has advised over twenty students including PhD candidates like Ian Briggs and numerous MS and BS students. His advising spans theoretical topics in programming languages and practical applications in web browsers and numerical computing. Panchekha leads research groups focused on programming languages applications to web browsers and numerical analysis. His work on the Herbie tool for floating-point accuracy improvement has become influential in the programming languages community, and his more recent work on browser internals is shaping how researchers understand and optimize modern web rendering engines. He is currently developing a textbook on web browsers that aims to synthesize knowledge about browser architecture and implementation.
Wooram Park is an Associate Professor in the Department of Mechanical Engineering at the University of Texas at Dallas (UT Dallas), affiliated with the Erik Jonsson School of Engineering and Computer Science. He leads the Robotics and Intelligent Systems Laboratory (ROBINS Lab) and holds a PhD from Johns Hopkins University (2008), along with MS and BS degrees from Seoul National University (2003 and 1999). His research focuses on robotics, biomedical robotics, computational structural biology, and image processing. Key projects include flexible needle steering for medical applications, haptic feedback systems, and advanced algorithms for motion planning and image reconstruction. He has received notable awards such as the Creel Fellowship (2007) and Critics’ Choice Award in ArtBot Design (2004). His work spans theoretical contributions in stochastic systems and practical innovations like vibratory magnetic robots (Vimbot) and wearable haptic devices. The ROBINS Lab emphasizes interdisciplinary research at the intersection of mechanical engineering, computer science, and biomedical applications.
Isaac Goldbring is a Professor in the Department of Mathematics at the University of California, Irvine (UCI), where he is a leading member of the Logic and Foundations group. He also holds a courtesy appointment in the Department of Logic and Philosophy of Science. His research lies at the intersection of model theory, operator algebras, and nonstandard analysis, with significant contributions to combinatorial number theory and quantum complexity theory. His research interests include: Model theory, particularly continuous and metric model theory Applications of nonstandard analysis to algebra, analysis, and combinatorics Tracial von Neumann algebras and the Connes Embedding Problem Operator algebras and their logical properties Combinatorial number theory and ultrafilters Lie theory and geometric group theory Goldbring’s recent publications reflect a strong trend in applying model-theoretic tools to deep problems in operator algebras and quantum information. His work on the Connes Embedding Problem, especially in connection with the MIP*=RE result, has provided simpler, more direct model-theoretic proofs and stronger refutations. He has also contributed to the logical undecidability of operator algebraic properties and the model theory of C*-algebras and W*-probability spaces. His notable scientific contributions include editing the volume Model Theory of Operator Algebras and authoring influential books such as Ultrafilters throughout Mathematics and Nonstandard Methods in Ramsey Theory and Combinatorial Number Theory . He is the Editor-in-Chief of the Journal of Logic and Analysis . Goldbring currently holds an NSF grant on model theory, quantum complexity, and embedding problems in operator algebras. He has mentored several graduate students, including Ryan Burkhart, Alec Fox, Michael Hehmann, Jennifer Pi, and Jessica Schirle. He has organized major conferences, such as the 2023 North American Annual Meeting of the Association for Symbolic Logic at UCI, and frequently gives invited lectures worldwide. He is actively involved in collaborative research with prominent mathematicians such as Bradd Hart, Ilijas Farah, and Lou van den Dries, and has delivered lecture series at institutions like Yonsei University and the National University of Singapore.
Oliver Nash is a researcher at Imperial College London, actively engaged in the formalisation of advanced mathematical concepts. His work bridges geometry and computational logic, with a focus on rigorous proof systems. Research Interests: Oliver's research lies at the intersection of geometry and the formalisation of mathematics. He specialises in using proof assistants to verify deep mathematical results, including topics such as the h-principle, sphere eversion, and Lie algebras. His work contributes to the growing field of certified mathematics, ensuring correctness through machine-checked proofs. Publication Trends: His recent publications at the CPP conference demonstrate a consistent focus on formalising foundational results in differential geometry and algebra. These works reflect a trend toward computational trust in mathematical proofs, particularly in complex geometric transformations and algebraic structures. Professional Activities: Oliver is an active contributor to the Certified Programs and Proofs (CPP) conference, presenting cutting-edge work in formal verification. He maintains a personal website detailing both his academic contributions and early explorations in computer graphics, such as raytracing and radiosity rendering from the early 2000s. Labs and Projects: While specific lab affiliations are not mentioned, his work is closely aligned with research groups in formal methods and interactive theorem proving, likely involving tools like Lean, Coq, or Isabelle.
YooJung Choi is an Assistant Professor at the School of Computing and Augmented Intelligence, Arizona State University. Her research focuses on probabilistic machine learning, trustworthy AI, and tractable probabilistic modeling. She holds a PhD in Computer Science from UCLA and has been recognized with awards like the Cisco Research Award and Simons-Berkeley Research Fellowship. Education: PhD in Computer Science (University of California, Los Angeles). Research interests include probabilistic reasoning, fairness, robustness, and interpretability. Her work bridges theoretical foundations and practical applications, with contributions to probabilistic circuits and optimal transport. Notable achievements include co-organizing TPM 2024 and presenting at venues like NeurIPS and AAAI. She actively promotes fairness in AI through frameworks that address label bias and discrimination patterns. Awards: Cisco Research Award, Simons-Berkeley Fellowship, AAAI 2023 New Faculty Highlights. Teaching: Courses on artificial intelligence, machine learning, and research supervision. Service: Tutorial leadership on probabilistic circuits, workshop organization, and academic talks globally.
Grant Weddell is an Associate Professor in the David R. Cheriton School of Computer Science at the University of Waterloo. His research focuses on database technology for real-time applications, including large-scale schema management, information clustering, dependency theory, and query optimization for heterogeneous data sources. He teaches courses such as CS338 (Introductory Databases), CS348 (Advanced Databases), CS446 (Software Engineering), and CS848 (Advanced Database Systems). His research interests emphasize the interplay between description logics and database systems, particularly in optimizing query processing and managing complex schemas. Recent work explores path agreements, functional dependencies, and ontology-mediated querying to enhance data integration and schema management efficiency. Teaching responsibilities include foundational database courses (CS338/348), software engineering (CS446), and advanced topics in information integration (CS848). No scientific awards are explicitly listed, though his contributions to database theory and optimization are extensive.
Andreas Abel is a Senior Lecturer in the Division of Computing Science at the Department of Computer Science and Engineering, Chalmers University of Technology and the University of Gothenburg. He has previously served as an Assistant Professor at Ludwig-Maximilians-Universität (LMU) Munich and has been a visiting researcher at INRIA in Paris. His primary affiliations are with Chalmers and the University of Gothenburg, where he conducts research and teaches in programming languages and type theory. Chalmers University of Technology, Department of Computer Science and Engineering, Senior Lecturer University of Gothenburg, Division of Computing Science LMU Munich, Assistant Professor (former) INRIA Paris, Visiting Researcher Abel’s research lies at the intersection of type theory, functional programming, and formal verification. He is particularly known for his work on dependent types, normalization by evaluation, and the development of the Agda proof assistant. His interests include constructive logic, logical frameworks, modal and linear typing, program verification, and compiler construction. He leads the Modal Dependent Type Theory project funded by the Swedish Research Council (Vetenskapsrådet) and has contributed to several other major research initiatives in programming language theory. His recent publications reflect a strong focus on foundational aspects of type systems, including cubical type theory, decidability of conversion, and formalization of algebraic completeness. These works appear in top-tier venues such as ICFP, LICS, POPL, and TYPES, showcasing both theoretical depth and practical implementation in Agda. Distinguished Paper Award, ICFP 2019 Editor, Theoretical Pearls column, Journal of Functional Programming Member, IFIP WG 1.3 on Foundations of System Specification Abel actively supervises students and contributes to the research community through program committee memberships for major conferences including LICS, ICFP, and CPP. He is a senior developer of Agda and the maintainer of the BNFC (Backus-Naur Form Compiler) tool. His work bridges theoretical computer science with practical software development for formal methods. He is involved in several research groups and projects, including the Programming Logic Group at Chalmers and the international EUTYPES network. His role as principal investigator and core contributor in multiple funded projects highlights his leadership in the field of programming language foundations.
Dr. Farzaneh Derakhshan is an Assistant Professor in the Computer Science Department at Illinois Institute of Technology (Illinois Tech), where she explores logical foundations of concurrency and develops formal methods for program verification. She earned her Ph.D. in Pure and Applied Logic from Carnegie Mellon University in 2021 under Frank Pfenning, followed by a postdoctoral fellowship at CMU with Limin Jia and Stephanie Balzer. Current affiliation: Illinois Tech (since ~2021) Previous affiliation: Carnegie Mellon University (Ph.D. and postdoc) Research focus: Type theory, logical verification, and security for concurrent systems Teaching: Courses on programming languages, type systems, and security Her research addresses fundamental challenges in concurrent programming, including: Developing modal logic frameworks for system verification Designing type systems for intermittent computing Creating behavioral type systems for security guarantees Applying relational logic to GPU security and secure compilation Investigating logical foundations of session-typed processes Formal verification of cyclic process networks Current research trends include: Hybrid dynamic verification for parallel systems Logical approaches to side-channel security Formal methods for cyber-physical systems Crash-resilient computing models Security verification in decentralized applications Noninterference proofs in session-typed concurrency Scientific recognition: NSF SaTC CORE Collaborative Award #2350217 Organizing committee member at Dagstuhl Seminar 26071 Professional leadership: Program committee co-chair for PLACES 2025 Committee roles at LICS 2026, ESOP 2026, ICFP 2025, and ECOOP 2025 Regular reviewer for ACM Transactions journals Laboratory involvement: Co-director of behavioral types research at Illinois Tech Collaboration with Carnegie Mellon's formal verification group Key participant in the FACCT workshop
Andrea Costamagna is a researcher affiliated with the École Polytechnique Fédérale de Lausanne (EPFL), working within the School of Computer and Communication Sciences and the Department of Communication Systems. His research focuses on logic synthesis, digital circuit design, and the intersection of machine learning with hardware implementation. His work includes optimizing digital circuits using techniques like resynthesis, resubstitution, and decomposition, with applications in FPGA design and low-power systems. Recent publications explore symmetry-based synthesis, glitch-aware power minimization, and the use of resistive switching devices in machine learning hardware. His research also extends to quantum physics modeling with deep learning.
Ori Lahav is a faculty member in the School of Computer Science at Tel Aviv University. His research is generously supported by an ERC Starting Grant and an ISF Grant. He actively supervises PhD and MSc students, and seeks highly motivated candidates for postdoc, PhD, and MSc positions in programming language theory, concurrency, and formal methods. Dr. Lahav completed his PhD at Tel Aviv University under the supervision of Arnon Avron. In 2014, he was a postdoctoral researcher at Tel Aviv University hosted by Mooly Sagiv. From 2014 to September 2017, he was a postdoctoral researcher at MPI-SWS in Germany hosted by Viktor Vafeiadis and Derek Dreyer. His primary research areas focus on programming languages and verification, with specialization in concurrency and relaxed memory models. He also has significant interests in proof-theory, semantics of non-classical logics, and automated reasoning. His work bridges theoretical foundations with practical applications in programming language design and implementation. Dr. Lahav's publication record shows a consistent trajectory of high-impact research in top-tier conferences including PLDI, POPL, OOPSLA, and ESOP. His recent work (2023-2025) demonstrates continued leadership in memory models, concurrency semantics, and verification techniques. His research spans both theoretical contributions in denotational semantics and practical tools for verification. Best Paper Award DISC 2024 Best Student Paper Award DISC 2024 Distinguished Artifact Award ESOP 2022 Distinguished Paper Award OOPSLA 2021 Kleene Award for Best Student Paper LICS 2013 Dr. Lahav actively advises students including Yoav Ben Shimon, Yotam Dvir, Amir Karniel, and Roy Margalit (PhD students), Yuval Katsman Ezra (MSc student), and has alumni including Ori Saporta (MSc) and Abhishek Kr Singh (postdoc, now Assistant Professor at IIIT Hyderabad). He has organized significant events including VMCAI 2024 and Dagstuhl Seminars on persistent programming. His teaching portfolio includes courses on Shared Memory Concurrency Semantics, Programming Language Foundations, and Software Foundations in Coq.
Thomas Scanlon is Professor of Mathematics at the University of California, Berkeley and serves as Vice-Chair for Graduate Affairs in the Berkeley Senate. He is additionally affiliated with the campus-wide Group in Logic and the Methodology of Science. His research lies at the intersection of mathematical logic and number theory, with a focus on model theory and its applications to diophantine geometry, difference and differential algebra, and arithmetic dynamics. Education S.B., University of Chicago, 1993 Ph.D., Harvard University, 1997 Research Interests Scanlon’s work centers on model theory , especially o-minimality , stability theory , and geometric model theory . He applies these logical tools to problems in diophantine geometry such as the André–Oort and Zilber–Pink conjectures, studies difference and differential algebraic structures, and investigates arithmetic dynamics of rational maps and Drinfeld modules. Publications Overview Since 1997 he has authored or co-authored more than sixty research papers. Recurring themes include the model theory of valued and difference fields, jet and prolongation spaces, effective bounds in diophantine problems, and functional transcendence results. Recent work (2018-2025) explores differential Chow varieties, strong minimality of modular functions, effective elimination procedures for differential-difference equations, and uniformity questions in diophantine geometry. Doctoral Supervision Scanlon has supervised at least sixteen Ph.D. theses at UC Berkeley, covering pure model theory, diophantine geometry, differential algebra, and stability theory. Students graduated between 2002 and 2022 include Alice Medvedev, Dragos Ghioca, Alex Kruckman, and Benjamin Castle. Contact & Office Email: scanlon@math.berkeley.edu Office: 723 Evans Hall, UC Berkeley Phone: (510) 642-3665
