جست‌وجوی استاد و پژوهشگر

Nadia Polikarpovaمشاهده پروفایل

دانشیار

• Program Synthesis
• Program Verification
• Type Systems
• +۵ مورد دیگر

Nadia Polikarpova is an Associate Professor in the Department of Computer Science and Engineering at the University of California, San Diego . She earned her PhD from ETH Zurich in 2014 under Bertrand Meyer , followed by postdoctoral research at MIT CSAIL with Armando Solar-Lezama . Her academic contributions have been recognized with prestigious awards including the 2020 Sloan Fellowship , 2020 Intel Rising Stars Award , and 2020 NSF CAREER Award . Polikarpova's research focuses on program synthesis , program verification , and type systems . She leads the Programming Systems group at UCSD and contributes to the IFIP Working Group 2.8 on Functional Programming since 2022. Her work spans foundational research and practical tools, including projects like Synquid , SuSLik , and Laurel that combine formal methods with machine learning for code generation. Her recent publications in venues like OOPSLA , NeurIPS , and ICFP reveal trends in AI-assisted programming , live programming environments , and formal verification . She has advised numerous PhD and Master’s students including Shraddha Barke , Zheng Guo , and Tristan Knoth , many of whom have moved to prominent academic and industry positions. Notable artifacts from her lab include tools like ColDeco for spreadsheet inspection and Superfusion for eliminating intermediate data structures. 2020 : Sloan Fellow 2020 : Intel Rising Stars Award 2020 : NSF CAREER Award 2021 : Distinguished Paper at POPL 2023 : Distinguished Artifact at PLDI 2023 : Distinguished Paper at OOPSLA Polikarpova actively contributes to academic service, serving on program committees for PLDI , POPL , and OOPSLA , and co-chairing the OOPSLA Review Committee in 2023. She has delivered keynotes at APLAS'20 and PLDI'24 , emphasizing the integration of large language models with formal methods.

Yin Tat Leeمشاهده پروفایل

دانشیار

• Convex Optimization
• Convex Geometry
• Graph Algorithms
• +۲ مورد دیگر

Yin Tat Lee is an Associate Professor at the Paul G. Allen School of Computer Science & Engineering , University of Washington, and a Senior Principal Researcher in Microsoft AI. His research spans convex optimization , convex geometry , graph algorithms , online algorithms , and differential privacy , with applications in machine learning and theoretical computer science.

Assia Mahboubiمشاهده پروفایل

پژوهشگر

• Type Theory
• Formal Verification
• Computer-Aided Mathematics
• +۳ مورد دیگر

Assia Mahboubi is a tenured researcher ( directrice de recherche ) at INRIA in the Gallinette team, Nantes, France, and an endowed professor in the Algebra and Number Theory section of the Vrije Universiteit Amsterdam, Netherlands. Her work bridges theoretical computer science and formal mathematics, with significant contributions to proof assistants and formal verification. Her research focuses on the foundations and formalization of mathematics in type theory, particularly on the automated verification of mathematical proofs. She explores the interplay between computer algebra and formal proofs, and is a key contributor to the Rocq prover (formerly Coq) and the Mathematical Components libraries. Her work often examines how familiar mathematical objects can be optimally represented for computer-aided proof checking. Recent publications show a strong trend toward categorical reasoning, diagram chasing, and continuity properties in constructive type theory, with increasing focus on practical applications of formal methods in computational mathematics. Her work demonstrates the maturation of formal verification techniques from theoretical foundations to practical tools for mathematical research. ERC Consolidator grant for the FRESCO (Fast and Reliable Symbolic Computation) project Mahboubi actively supervises doctoral students including Vojtěch Štěpančík, Tomás Vallejos Parada, and Alain Chavarri Villarello. She has received significant research funding through her ERC Consolidator grant for the FRESCO project, which aims to develop fast and reliable symbolic computation techniques. She is deeply involved in the international research community, serving on program committees for major conferences including POPL, CPP, and ICFP. She leads research in the Gallinette team at INRIA, which focuses on the intersection of proof assistants, programming languages, and formal mathematics. Her work has helped establish formal verification as a practical tool for mathematical research, moving beyond theoretical foundations to real applications in computational mathematics.

• Secure Decentralized Systems
• Blockchain Technology
• Systems Security
• +۳ مورد دیگر

Prof. Bryan Ford leads the Decentralized/Distributed Systems (DEDIS) lab at EPFL. He focuses on secure decentralized systems, including blockchain technology, privacy, and systems security. He earned his Ph.D. from MIT and held faculty positions at Yale University and EPFL. His work spans distributed consensus protocols, peer-to-peer networking, and privacy-preserving systems. Key projects include QuePaxa (timeout-free consensus), UIA (global connectivity for mobile devices), and MedCo (secure healthcare data sharing). He advises numerous PhD students and contributes to open-source projects like Bitcoin collective signing and privacy networks like Riffle. Education: Ph.D., MIT; Postdoctoral work at Yale Research interests include blockchain scalability, consensus algorithms, and cryptographic privacy. His lab develops systems like TRIP for coercion-resistant voting and F3B to mitigate blockchain front-running. His work on NAT traversal and peer-to-peer protocols (e.g., STUN/ICE) remains foundational in network architecture. He emphasizes practical, auditable security solutions such as CertiKOS and atomic cross-chain transactions (Atom). Notable contributions: CoSi (collective signing), OmniLedger (sharded blockchain), and privacy-preserving protocols like PURBs (Protected Unsealable Recursive Boxes). His lab collaborates with Swiss Post to audit e-voting systems and designs democratic cryptocurrencies like PoPCoin.

Zachary Kincaidمشاهده پروفایل

دانشیار

• Program Analysis
• Formal Methods
• Programming Languages
• +۴ مورد دیگر

Zachary Kincaid is an Associate Professor in the Department of Computer Science at Princeton University's School of Engineering and Applied Science. His research focuses on program analysis, logic, and programming languages, with an emphasis on making program analysis compositional and robust. He received his PhD from the University of Toronto under the supervision of Azadeh Farzan. His work has been implemented in the Duet program analyzer, and he has an Erdős number of 3. Dr. Kincaid's research interests include: Compositional program analysis techniques Algebraic approaches to program analysis Termination analysis and ranking function synthesis Verification of concurrent and parallel programs Automated reasoning and decision procedures Analysis of numerical programs and loops His recent publications show a strong focus on developing novel techniques for program analysis that bridge theoretical computer science with practical verification tools, particularly in nonlinear analysis, quantified reasoning, and compositional verification. Dr. Kincaid has received research support from ONR grant N00014-19-1-2318 for his work on robust program analysis. He has advised graduate students including: Current: Jake Silverman, Nicolas Koh, Nikhil Pimpalkhare Graduated: Shaowei Zhu (PhD 2024, Researcher at Amazon), Charlie Murphy (PhD 2023, Postdoc at University of Wisconsin–Madison) Dr. Kincaid teaches courses including: COS 320 – Compiling Techniques (Spring 2024, 2022, 2020, 2019) COS 516 / ELE 516 – Automated Reasoning about Software (Fall 2025, 2022, 2018) COS 217 – Introduction to Programming Systems (Fall 2024) COS IW – Practical Solutions to Intractable Problems (Fall 2023, Spring 2023, 2018, 2017) COS IW – Little Languages (Spring 2018) COS 597D – Reasoning about concurrent systems (Fall 2016)

Bo Xiongمشاهده پروفایل

پژوهشگر

• Machine Learning
• Knowledge Graphs
• Graph Neural Networks
• +۴ مورد دیگر

Bo Xiong is a researcher at the University of Stuttgart in the Analytic Computing group. His research focuses on machine learning and knowledge graphs , with a particular emphasis on geometric embeddings and hyperbolic neural networks. His research interests include: Knowledge graph embeddings Hyperbolic and pseudo-Riemannian geometry in AI Temporal knowledge graph reasoning Structured multi-label prediction Recent publications highlight his work on geometric relational embeddings, complex query answering, and temporal fact reasoning using advanced manifold-based techniques.

• Quantum Computing
• Quantum Foundations
• ZX-calculus
• +۷ مورد دیگر

John van de Wetering is an Assistant Professor at the Theoretical Computer Science group of the Informatics Institute, University of Amsterdam, working with the QuSoft research center. He co-authored the open-access book Picturing Quantum Software and developed the PyZX quantum compiler. His research spans quantum computation and quantum foundations, focusing on diagrammatic methods like the ZX-calculus and ZH-calculus. Quantum circuit optimization and verification Quantum foundations via algebraic/compositional methods Co-creator of PyZX His recent publications explore multi-qutrit systems, completeness of graphical calculi, and quantum state representations. Supervises students in quantum computing, including Lia Yeh and Sarah Li. Directs the new Master's program in Quantum Computer Science at UvA. Actively contributes to open-source projects and international conferences. Notable collaborations include Aleks Kissinger, Neil J. Ross, and QuSoft researchers. Uses GitHub for DiZX development (qudit extension of PyZX). No explicit scientific awards mentioned.

Michael D. Ernstمشاهده پروفایل

استاد

• software engineering
• programming languages
• type theory
• +۶ مورد دیگر

Michael D. Ernst is a Professor in the Computer Science & Engineering department at the University of Washington's College of Engineering. His research aims to make software more reliable, more secure, and easier (and more fun!) to produce. Previously, he was a tenured professor at MIT and a researcher at Microsoft Research. Ernst's primary technical interests are in software engineering, programming languages, type theory, security, program analysis, bug prediction, testing, and verification. His research combines strong theoretical foundations with realistic experimentation, with an eye to changing the way that software developers work. He focuses particularly on programmer productivity and developing practical tools that can be integrated into developers' workflows. Analysis of his recent publications (2018-2025) reveals a continued focus on verification techniques, program analysis, and testing methodologies. His work spans from theoretical foundations of type systems to practical applications of NLP for test generation and LLMs for test oracle creation. A consistent theme is developing lightweight, modular approaches that can be practically applied in real-world development environments. Scientific Awards: ACM Fellow (2014) John Backus Award (2009) NSF CAREER Award (2002) ACM SIGSOFT Impact Paper Award (2013) 8 ACM Distinguished Paper Awards across multiple conferences ECOOP 2011 Best Paper Award Microsoft Academic Search ranked #2 in software engineering research (2013) Ernst has received significant research funding including the NSF CAREER Award, supporting his work on program analysis and verification techniques. His research combines theoretical rigor with practical impact, often resulting in tools that are adopted by the software engineering community. He actively collaborates with researchers across institutions and has served in leadership roles for major conferences in programming languages and software engineering. His research group develops practical tools that address real challenges in software development, with a focus on making verification and analysis techniques more accessible to working developers. Current projects include applying machine learning techniques to software engineering problems while maintaining strong theoretical foundations.

Dominique Devrieseمشاهده پروفایل

استاد

• Functional Programming
• Object Capabilities
• Secure Compilation
• +۵ مورد دیگر

Dominique Devriese is a professor at the Department of Computer Science, KU Leuven, and a member of the DistriNet research group. His work bridges computer security, programming languages, and formal verification. Research interests: Functional Programming, Object Capabilities, Secure Compilation, Dependently-typed Programming, Modal Type Theory Teaching: Formal Systems, Object-Oriented Programming, CyberSecurity, Secure Software His research focuses on rigorous software systems security through capability machines and secure compilation techniques. He actively contributes to formal verification using Agda and Haskell, with recent work on multimode type theory and effect parametricity. Key publication trends include: multimode/presheaf type theory, capability-based security models, formal verification of hardware/software abstractions, and parametricity applications in programming languages. Contact: Email: dominique.devriese@kuleuven.be ORCID: 0000-0002-3862-6856

Dmitriy Traytelمشاهده پروفایل

دانشیار

• Logic
• Automata Theory
• Runtime Verification
• +۷ مورد دیگر

Dmitriy Traytel is an Associate Professor at the University of Copenhagen's Department of Computer Science since August 2020, where he currently heads the Software, Data, People & Society (SDPS) section. Prior to this position, he worked as a senior researcher (Oberassistent) in the Information Security Group led by David Basin at ETH Zürich. He completed his PhD at TU München under Tobias Nipkow's supervision in 2015. His research focuses on formal methods, particularly logic, automata theory, runtime verification and monitoring, decision procedures, (co)induction and (co)recursion, and interactive theorem proving. Traytel develops formally verified tools for runtime monitoring including VeriMon, TimelyMon, and WhyMon, emphasizing correctness and efficiency in monitoring complex temporal properties. His recent publications (2021-2025) demonstrate a strong focus on first-order temporal logic monitoring, with particular attention to explainable verdicts, scalable parallel implementations, and formal verification of monitoring algorithms. The work spans theoretical foundations in logic and category theory while maintaining practical applications in runtime verification systems. Distinguished Paper Award at POPL 2025 for 'Barendregt Convenes with Knaster and Tarski' Best Student Paper Award at FSCD 2016 Distinguished Paper Award at ATVA 2018 Traytel has supervised numerous PhD, Master's, and Bachelor's students in areas spanning formal verification, runtime monitoring, and theorem proving. His research has been supported through collaborations with major institutions including ETH Zürich and TU München. He actively contributes to the academic community by serving on program committees for major conferences including ITP 2025 and RV 2025. He leads the Software, Data, People & Society section at the University of Copenhagen, focusing on developing formally verified tools for runtime verification that bridge theoretical computer science with practical applications in security and system monitoring.

Martín Hötzel Escardóمشاهده پروفایل

استاد

• Homotopy Type Theory
• Univalent Mathematics
• Martin-Löf Type Theory
• +۱۲ مورد دیگر

Martín Hötzel Escardó is a Professor of Theoretical Computer Science in the School of Computer Science at the University of Birmingham, UK. He has been a faculty member since 2000, following previous academic positions at Imperial College London, the University of Edinburgh, and the University of St Andrews. His research bridges theoretical computer science and pure mathematics, with a strong emphasis on foundational aspects of computation. His educational background includes a BSc and MSc from Universidade Federal do Rio Grande Sul (Brazil) and a PhD from Imperial College London (1997) under Michael B. Smyth. Escardó's research interests center on topology in computation , constructive mathematics , dependent and univalent type theory (including Homotopy Type Theory and Cubical Type Theory), domain theory , locale theory , and exact real-number computation . His work explores deep connections between logic, topology, and programming, often using functional languages like Haskell and Agda to formalize and experiment with theoretical ideas. He is particularly known for his discoveries on exhaustively searchable infinite sets and the topological nature of computability. The trend in his recent publications reflects a sustained focus on univalent foundations, constructive domain and order theory, game semantics with dependent types, and the logical structure of type universes. His work consistently advances the formalization and understanding of higher-type computation and constructive mathematics within modern type theories. He has no listed scientific awards in the provided text, but his influence is evident through his extensive publication record and software developments like TypeTopology. Escardó has advised several students and collaborators, though specific names are not listed. He has been involved in significant research projects, particularly in the formalization of mathematics in type theory and the semantics of programming languages. His work often involves developing Agda libraries to formalize new mathematical results constructively. He leads and contributes to a vibrant research group in theoretical computer science at Birmingham, with a focus on logic, semantics, and type theory. His public research blog, lecture notes, and open-source Agda code (e.g., TypeTopology, HoTT-UF-in-Agda) serve as important resources for the community.

Farzaneh Derakhshanمشاهده پروفایل

استادیار

• Type Theory
• Proof Theory
• Programming Languages
• +۷ مورد دیگر

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

Steve Zdancewicمشاهده پروفایل

استاد

• Programming Languages
• Type Theory
• Logic
• +۷ مورد دیگر

Steve Zdancewic is the Schlein Family President's Distinguished Professor and Associate Chair in the Department of Computer and Information Science at the University of Pennsylvania's School of Engineering and Applied Science. He is a leading researcher in programming languages, formal methods, and computer security with over two decades of impactful contributions to the field. His research interests span programming languages, type theory, logic, computer security, quantum programming, and formal verification. Zdancewic has made significant contributions to information-flow security, memory safety, program synthesis, and the verification of low-level systems. His work often bridges theoretical foundations with practical applications, particularly through the development of verified systems using Coq and other proof assistants. Analysis of his recent publications reveals a strong focus on formal verification techniques, particularly using Interaction Trees and the Coq proof assistant. His research trajectory shows consistent evolution from foundational work on information-flow security toward increasingly sophisticated verification of complex systems including LLVM, quantum computing, and distributed systems. His work demonstrates a commitment to building practically useful verification tools while maintaining rigorous theoretical foundations. Distinguished Paper Award for Semantics for Noninterference with Interaction Trees (ECOOP 2023) Schlein Family President's Distinguished Professor (2021) Distinguished Paper Award for Interaction Trees (POPL 2020) Christian R. and Mary F. Lindback Foundation Award for Distinguished Teaching (2018) IEEE MICRO top picks (2013) Alfred P. Sloan Fellow (2009-2010) NSF CAREER award (2004) Zdancewic has advised numerous PhD students who have gone on to successful careers in academia and industry. His research has been supported by significant grants from NSF, including the NSF Expedition on the Science of Deep Specification. He is actively involved in multiple major research projects including Vellvm (verified LLVM), DeepSpec, and quantum programming verification. Zdancewic also co-organizes Penn's PL Club programming languages research group with Benjamin Pierce and Stephanie Weirich.

Ori Lahavمشاهده پروفایل

دانشیار

• Programming Languages
• Verification
• Concurrency
• +۴ مورد دیگر

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.

Tobias Nipkowمشاهده پروفایل

استاد

• Formal Methods
• Interactive Theorem Proving
• Program Verification
• +۹ مورد دیگر

Professor Tobias Nipkow is a leading researcher in formal methods and interactive theorem proving at the Technical University of Munich (TUM), affiliated with the School of Computation, Information and Technology and the Department of Computer Science. He is a core developer of the Isabelle proof assistant and leads the Theorem Proving Group. His work has profoundly influenced program verification, semantics, and formalized mathematics. University: Technical University of Munich School: School of Computation, Information and Technology Department: Department of Computer Science Research Group: Theorem Proving Group Key Projects: Isabelle, Archive of Formal Proofs, Concrete Semantics His research focuses on formal verification, higher-order logic, semantics of programming languages, and verified algorithms. He has pioneered the formalization of textbook algorithms, data structures like B+-trees and quadtrees, and logical systems. His work bridges theoretical foundations with practical tools for software correctness. The most recent publications show a strong trend in verifying classical algorithms (e.g., Gale-Shapley, Earley parser), data structures (B+-trees, deques), and decision procedures, primarily using Isabelle/HOL. His contributions span foundational logic, program analysis, and educational approaches to formal methods. Best Paper Award at CADE 28 (2021) Tobias Nipkow has made extensive contributions to advising and collaborative research, co-authoring with numerous researchers and students. He has secured support for large-scale formalization efforts and contributed to major projects like the Flyspeck proof of the Kepler conjecture. His work is supported by ongoing development of the Isabelle framework and the Archive of Formal Proofs. He leads the Theorem Proving Group at TUM, which is central to the development and application of Isabelle. The group fosters international collaboration, contributes to the Archive of Formal Proofs, and advances research in automated reasoning, semantics, and verified systems.