Fredrik Kjolstad is an Assistant Professor in the Department of Computer Science at Stanford University, specializing in compilers and programming models for sparse computing and performance engineering. His research focuses on separating algorithms from data representations to enable portable applications across diverse hardware platforms. His research interests span compilers, programming models, performance engineering, and computer architecture, with particular emphasis on sparse tensor algebra, compiler design for heterogeneous systems, and high-performance computing. He has pioneered frameworks like TACO, Simit, and Distal that enable efficient sparse computations across CPUs, GPUs, and specialized accelerators. Dr. Kjolstad's publications demonstrate expertise in compiler optimization techniques for sparse data structures, tensor algebra, and distributed systems. His work consistently addresses the challenge of bridging high-level programming abstractions with efficient hardware execution across diverse architectures. MIT EECS First Place George M. Sprowls PhD Thesis Award NSF CAREER Award Rosing Award Adobe Fellowship Google Research Scholarship Best Paper Awards at EuroMPI 2013, OOPSLA 2017, and OOPSLA 2021 ISCA Distinguished Artifact Award PLDI and OOPSLA Distinguished Paper Awards He advises multiple PhD students including James Dong, Olivia Hsu, and Rohan Yadav, while leading research on compiler technologies that have received significant grant support. His group develops practical tools like the TACO compiler and Legate Sparse that are used in both academic and industrial settings. Current projects focus on programmable accelerators for sparse tensor algebra, distributed sparse computing, and compiler support for emerging hardware architectures.
Anil Madhavapeddy is the Professor of Planetary Computing at the University of Cambridge Computer Laboratory, where he co-leads the Energy & Environment Group and is a member of the Systems Research Group. He is also a Fellow at Pembroke College where he serves as Director of Studies in Computer Science. Madhavapeddy completed his PhD from the University of Cambridge in 2003 and his BEng in Information Systems Engineering from Imperial College in 1999. He holds a JM Keynes Fellowship since 2022 for his work combining computer science with economics, and serves on the management committee of the Cambridge Conservation Initiative where he co-directs 4C (Cambridge Centre for Carbon Credits) and the Centre for Earth Observation. His research spans computer systems and programming languages with a strong focus on applying these technologies to global conservation, biodiversity, and climate change challenges. He leads the OCaml Labs group and has made significant contributions to open-source projects including OCaml, Docker, Xen, and OpenBSD. His work often bridges computer science with environmental science, developing computational approaches to address planetary-scale challenges. Madhavapeddy's recent publications demonstrate a clear trajectory toward integrating programming language research with environmental monitoring and conservation. His work spans from foundational programming language techniques to applied geospatial computing systems, with increasing emphasis on biodiversity measurement, carbon credit systems, and planetary-scale environmental monitoring. JM Keynes Fellowship (2022-present) As an educator, Madhavapeddy teaches undergraduate courses including Foundations of Computer Science, Software & Security Engineering, and Cloud Computing. He mentors MPhil and PhD students and co-founded the award-winning book 'Real World OCaml' (2nd Edition, 2022). He has co-founded several companies including Unikernel Systems, High Energy Magic, Segfault, and Tarides to translate research into real-world impact. Madhavapeddy leads the OCaml Labs group at Cambridge and works closely with the Energy & Environment Group, collaborating with colleagues from Plant Sciences, Zoology, Economics, and NGOs including UNEP-WCMC and the IUCN. His current efforts are primarily focused on conservation technology through partnerships with organizations like Canopy PACT.
Umang Mathur is a Presidential Young Professor (Assistant Professor) in the School of Computing at the National University of Singapore (NUS), where he leads the FOCS Lab and is affiliated with PLSE@NUS (Programming Languages and Software Engineering group). He has established himself as a leading researcher in Formal Methods, with significant contributions to concurrency analysis and program verification. Dr. Mathur received his PhD from the University of Illinois at Urbana-Champaign under Prof. Mahesh Viswanathan. Prior to joining NUS, he worked as a Research Scientist at Facebook Inc. and as a Research Fellow at the Simons Institute for the Theory of Computing. His doctoral work was supported by a Google PhD Fellowship. PhD: University of Illinois at Urbana-Champaign Current Position: Presidential Young Professor at NUS School of Computing Previous Positions: Research Scientist at Facebook, Research Fellow at Simons Institute His research spans Formal Methods and Logic with applications to Programming Languages, Software Engineering, and Cyber-Physical Systems. Dr. Mathur specializes in developing algorithmic techniques for analysis of concurrent software and understanding decidability boundaries in verification and synthesis. His work bridges theoretical foundations with practical implementations, making verification techniques more efficient for real-world systems. Analysis of his recent publications reveals a strong focus on practical concurrency analysis, with many papers addressing race detection, deadlock prediction, and memory model verification. His research consistently demonstrates how theoretical computer science can solve practical software engineering challenges, particularly in making verification techniques scalable and efficient for industrial applications. Google PhD Fellowship ESEC/FSE 2018 Distinguished Paper Award ASPLOS 2022 Best Paper Award POPL 2023 ACM SIGPLAN Distinguished Paper Award CPP 2024 Distinguished Paper Award Dr. Mathur actively mentors numerous PhD students, Master's students, and undergraduates through the FOCS Lab. His research group has received support from Google Research grants and other funding sources. He serves on program committees for major conferences including PLDI, POPL, and ASPLOS, and has organized events like PLMW@PLDI. His teaching includes courses on Data Structures and Algorithms, Foundations of Logic in Computer Science, and advanced topics in Programming Languages. As director of the FOCS Lab, Dr. Mathur oversees a vibrant research group focused on foundational aspects of computer science with direct applications to programming languages and software engineering. The lab maintains strong international collaborations and regularly publishes in top-tier venues, reflecting its significant contributions to the field of formal methods and programming languages.
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.
Kunle Olukotun is a Professor of Electrical Engineering and Computer Science at Stanford University's School of Engineering, where he has been faculty since 1991. He directs the Stanford Pervasive Parallelism Lab (PPL) and co-leads the Transactional Coherence and Consistency (TCC) project. His research focuses on computer architecture, parallel programming environments, and scalable parallel systems. Key areas include chip multiprocessors (CMPs), transactional memory systems, domain-specific languages (DSLs) for heterogeneous computing, and hardware-software co-design for machine learning workloads. His work bridges theoretical foundations with practical systems implementation. Notable contributions include the Stanford Hydra research project (one of the first chip multiprocessors with thread-level speculation), founding Afara Websystems (acquired by Sun Microsystems), and developing the Niagara processor architecture. His DSL frameworks like Green-Marl and Spatial enable efficient graph analysis and hardware acceleration. His publications reveal strong trends in parallel systems evolution: from foundational CMP research (2000s) to transactional memory (2004-2010), then DSLs for heterogeneous computing (2010-2015), and currently foundation model systems (2023-2025). Subfield analysis shows consistent focus on hardware-software co-design, sparse computation, and compiler techniques across decades. ACM Fellow (2006) for contributions to multiprocessors on a chip and multi-threaded processor design Best Paper Award at IEEE International Symposium on Workload Characteristics (IISWC '10) for EigenBench Olukotun actively mentors researchers through the Stanford Pervasive Parallelism Lab (PPL), which seeks to proliferate parallelism across application domains. His projects have secured significant industry partnerships, including the acquisition of his startup Afara Websystems by Sun Microsystems. Current research focuses on compiler frameworks for foundation model systems and hardware acceleration for sparse machine learning workloads, supported by collaborations with major tech companies. He leads the Stanford Pervasive Parallelism Lab (PPL), which develops compiler and runtime systems for heterogeneous architectures. The lab's work spans DSLs, hardware acceleration, and parallel programming models, with strong industry ties to companies like NVIDIA and Google. Current initiatives include the Mosaic compiler framework and Stardust architecture for sparse tensor computation.
Fernando Magno Quintão Pereira is an Associate Professor at the Federal University of Minas Gerais (UFMG), Brazil, specializing in compiler design and program analysis. His academic journey began with a Ph.D. from UCLA in 2008 under Jens Palsberg's supervision, establishing his foundation in compiler research. His research focuses on compilers , with core expertise in code generation , compiler optimizations , and static program analyses . Recent work explores quantum compilation, binary analysis, and security-aware compilation techniques. His publications reveal consistent contributions to major conferences including PLDI, CGO, and SPLASH, with emphasis on practical optimization frameworks and theoretical compiler advancements. Analysis of his 15 most recent publications (2020-2026) shows dominant themes in binary optimization (e.g., AnghaBench), security-aware compilation (e.g., Memory-Safe Elimination of Side Channels), and emerging architecture support (e.g., Quantum Computing Compilation). His work bridges theoretical compiler principles with real-world systems challenges. He actively contributes to the academic community through: Program committees for PLDI (2020-2025), CGO (2021-2026), and SPLASH conferences Leadership roles including CGO Finance Chair (2026) and PLDI Diversity & Inclusion Co-Chair (2023-2024) Organizing JENSFEST 2024 and serving on multiple conference steering committees Pereira maintains an active research group evidenced by continuous publication output and conference leadership, with his personal website ( homepages.dcc.ufmg.br/~fernando/ ) serving as a hub for his academic activities.
Sean Kauffman is an Assistant Professor in the Department of Electrical and Computer Engineering at Queen's University, Faculty of Engineering and Applied Science. He holds his office in Walter Light Hall, Room 611, and can be reached at sean.k@queensu.ca or by phone at 613-533-6000 ext. 77360. Dr. Kauffman earned his Ph.D. in Electrical and Computer Engineering from the University of Waterloo before completing a two-year postdoctoral position at Aalborg University in Denmark. Notably, he returned to academia after accumulating over a decade of industry experience as a software engineer, with his final industry role being Principal Software Engineer at Oracle. His research expertise spans several critical areas in computer science and software engineering, with a particular focus on safety-critical software systems. His work significantly contributes to the fields of Formal Methods, Runtime Verification, Anomaly Detection, and Explainable AI. Dr. Kauffman has established productive research collaborations with prestigious organizations including NASA's Jet Propulsion Laboratory, the Embedded Systems Institute, QNX, and Pratt and Whitney Canada. Dr. Kauffman's research output demonstrates a consistent focus on event stream analysis, formal verification techniques, and the development of practical tools for system monitoring. His most notable contribution is the nfer language and toolset, which has become influential in the runtime verification community for its ability to abstract event streams into meaningful temporal hierarchies. His publications reveal a progression from theoretical foundations to practical implementations, with applications spanning spacecraft telemetry, autonomous vehicles, and embedded systems. Among his scientific contributions, Dr. Kauffman has received recognition for his work on the complexity analysis of nfer evaluation, developing methods for annotating control-flow graphs for formalized test coverage criteria, and creating frameworks for anomaly detection in embedded systems. His research has been published in top-tier venues including Science of Computer Programming, International Journal on Software Tools for Technology Transfer, and proceedings of major conferences like Runtime Verification and NASA Formal Methods. As an educator, Dr. Kauffman employs active learning techniques, productive failure approaches, and peer instruction to foster student engagement. His industry background informs his teaching approach, providing students with practical insights into real-world software engineering challenges, particularly in safety-critical domains. Dr. Kauffman leads the CritLab research group at Queen's University, which focuses on critical systems research. The lab develops tools and techniques for analyzing and verifying systems where failures could have severe consequences, with applications in aerospace, automotive, and other safety-critical domains. His work on the nfer language has spawned related projects including nvis for visualizing temporal interval hierarchies.
Tevfik Bultan is a Professor and Chair of the Department of Computer Science at the University of California, Santa Barbara. His research focuses on software verification, program analysis, software engineering, and computer security. He directs the Verification Laboratory (VLab) and has authored over 100 refereed publications. Education Ph.D. in Computer Science, University of Maryland, College Park (1998) M.S. in Computer Engineering, Bilkent University (1992) B.S. in Electrical Engineering, Middle East Technical University (1989) Research Focus Bultan's work spans automated verification techniques, security vulnerability detection, quantitative program analysis, and symbolic execution. His lab develops tools for analyzing software systems with applications in cloud security, network protocols, and embedded systems. Awards and Honors ACM Distinguished Scientist (2016) NSF CAREER Award (2000) UCSB Outstanding Graduate Mentor Award (2016) ACM SIGSOFT Distinguished Paper Awards (2005, 2014) NATO Science Fellowship (1993) Professional Activities He has chaired program committees for top conferences including ICSE, FSE, and ASE. Currently serves as associate editor for ACM TOSEM and on steering committees for ISSTA, ASE, and ICSE. Regularly advises PhD students and postdoctoral researchers in verification and security. Laboratory Leads the Verification Laboratory (VLab) focusing on automated reasoning techniques for software systems. Current projects include symbolic analysis for vulnerability detection, quantitative information flow, and security policy verification.
Vincent Weaver is an Associate Professor in the Electrical and Computer Engineering Department at the University of Maine's College of Engineering. He leads the VMW Research Group, focusing on low-level systems research including hardware performance counters, computer architecture, and operating systems. Weaver received his BS in Electrical Engineering from the University of Maryland College Park in December 2000, followed by MS (January 2009) and PhD (May 2010) degrees in Electrical and Computer Engineering from Cornell University. He joined the University of Maine faculty in July 2012 as an Assistant Professor and earned tenure and promotion to Associate Professor in September 2018. His research centers on hardware performance analysis, architectural simulation, and systems programming with emphasis on Linux kernel development and embedded systems. Weaver's work bridges theoretical computer architecture with practical systems implementation, often resulting in open-source tools that advance the field. His publications reveal a consistent focus on performance analysis techniques, code optimization, and security through low-level system understanding. Weaver maintains an active teaching schedule including courses in embedded systems, operating systems, and network engineering. He values students with strong programming skills and encourages open source contributions as part of the learning process. His research group provides hands-on experience with cutting-edge processor architectures and performance analysis tools.
Prof. Gerhard Dueck, a Professor, conducted a week-long research visit focused on quantum computing, delivering two technical talks on September 24th and 27th at an academic institution. His research expertise centers on: Quantum computing architecture optimization for IBM systems Eclipse OMR runtime programming support including JIT/AOT compilation Region-based garbage collection algorithms reducing global pauses CNOT gate efficiency and Toffoli circuit mapping for quantum hardware No scientific awards or student advising details were referenced in the provided context. His work demonstrates significant reductions in quantum circuit gate counts (up to 67%) through novel mapping methodologies targeting IBM's QX architectures.
Michael Pradel is a full professor in the Computer Science Department at the University of Stuttgart and faculty member at CISPA Helmholtz Center for Information Security (effective September 2025), where he leads the Software Lab. He is also affiliated with the International Max Planck Research School for Intelligent Systems and the Stuttgart ELLIS Unit, reflecting his interdisciplinary research approach. His research interests focus on software engineering, particularly program analysis, bug detection, and the application of machine learning to developer tools. Pradel's recent work increasingly explores LLM-based approaches for program repair, code analysis, and automated software development, as evidenced by projects like RepairAgent and ExecutionAgent. Pradel's publication record shows a clear trend toward integrating AI techniques with traditional software engineering methods, with recent papers focusing on LLM applications for program repair, change validation, and quantum software analysis. His work bridges theoretical foundations with practical tool development, as seen in frameworks like DyLin for Python analysis and LintQ for quantum programs. Ernst-Denert Software Engineering Award Emmy Noether grant (1.3 million Euro) by the DFG ERC Starting Grant (1.5 million Euro) Multiple ACM SIGSOFT Distinguished Paper Awards ACM Distinguished Member recognition Pradel actively mentors PhD students, with recent graduates including Matteo (specializing in quantum software) and Luca (focusing on software evolution). His group has received significant funding and maintains strong industry connections, including past sabbaticals at Facebook. He serves in leadership roles for major conferences, including PC co-chair for FSE 2027, demonstrating his standing in the software engineering community. The Software Lab maintains active collaborations with institutions worldwide, including CMU, Google, KAIST, and several European universities.
Jeremy G. Siek is a Professor at Indiana University Bloomington in the School of Informatics and Computing. His research spans programming language design, type systems, gradual typing, mechanized theorem proving, and optimizing compilers. Gradual typing integration in functional languages Co-inventor of the Boost Graph Library Former NSF CAREER award recipient Active in programming language foundations research Jeremy's research focuses on reconciling static and dynamic type checking through gradual typing, with current work on parametricity in polymorphic blame calculus, combining gradual typing with dependent types, and formal criteria for gradual type systems. He investigates high-performance implementations of gradual typing and its application to security enforcement. His recent publications examine verified nanopass compilers, gradual security guarantees, and parameterized cast calculi. He has received multiple distinguished visiting fellowships and maintains the Deduce proof assistant for educational use. NSF CAREER Award (2009) Distinguished Visiting Fellowships (2010, 2015) Jeremy leads the Center for Programming Systems at IU and advises Ph.D. students Tianyu Chen (gradual security) and Darshal Shetty (gradual dependent types). He teaches courses in compilers, data structures, and programming language foundations.
Andrew K. Hirsch is an Assistant Professor at the University at Buffalo, SUNY , Department of Computer Science and Engineering. He leads the Databases and Programming Languages group and focuses on programming languages for decentralized systems, particularly choreographic programming and information-flow security. Education: Ph.D. in Computer Science (2019) from Cornell University, supervised by Ross Tate on computational effects. B.S. in Computer Science and Pure Mathematics from The George Washington University. Research Interests: His work centers on choreographic programming, a paradigm ensuring deadlock-free concurrent systems, and information-flow security for decentralized applications. He also explores computational effects and type systems in programming language theory. Publications: Recent work includes advancements in process polymorphism (OOPSLA 2025), type-level polymorphism (PLACES 2025), and security definitions for higher-order declassification (OOPSLA 2023). Students: Doctoral: Michael Piskozub, Keith Allen Mason Masters: Alexander Bohosian, Gianna Bossoreale Undergraduate: Alex Doyoon Kim, Julia Montouri Recent Alumni: Ethan Canton, Tiffany Cai, Vamsi Krishna Bellam, Vincent Chan, Frank (Feng-Mao) Tsai Projects: Leads initiatives such as Choret (open choreographies) and The Pirouette Language and Compiler , which translate choreographic programs into concurrent system implementations.
Aymeric Fromherz is a researcher at Inria Paris, focusing on formal methods for secure systems. He leads projects in Rust verification, high-assurance cryptography, and formalization of computational legal texts. Education includes a PhD from Carnegie Mellon University (co-advised by Bryan Parno and Corina Păsăreanu) and degrees from École Normale Supérieure. His research spans Rust verification (via Aeneas toolchain), verified cryptographic primitives , and computational law (through the Catala language). Recent publications address memory allocators, borrow-checking, and legal ambiguity detection. Major Scientific Awards : Distinguished Artifact Award (CAV 2025) Best Tool Paper Award (ESOP 2024) ACM SIGSAC Dissertation Award (2021) A.G. Milnes Dissertation Award (2021) He contributes to conferences like POPL, ICFP, and CPP, and participates in the Everest Project. The Prosecco Team at Inria Paris supports his research on formal methods and security.
Matthew Fluet is an Associate Professor and Graduate Program Director in the Department of Computer Science at Rochester Institute of Technology's Golisano College of Computing and Information Sciences. He received his PhD in Computer Science from Cornell University and his BS in Mathematics from Harvey Mudd College. Prior to joining RIT, he was a research assistant professor at the Toyota Technological Institute at Chicago. Dr. Fluet's research focuses on programming languages, with particular emphasis on: Functional programming Compiler construction Program analysis Type systems Parallelism and concurrency His research has resulted in several significant projects including Manticore (a heterogeneous-parallel functional programming language), MaPLe/MPL (a functional language for provably efficient and safe multicore parallelism), and contributions to MLton (a whole-program optimizing Standard ML compiler). His work is supported by multiple National Science Foundation grants. Dr. Fluet has published extensively in top programming languages conferences including ICFP, POPL, PLDI, and PPoPP. His recent work focuses on automatic parallelism management, type-and control-flow analysis, and memory management for parallel systems, demonstrating a consistent research trajectory in making parallel programming safer and more accessible through language design. His notable research grants include: National Science Foundation (CISE Research Infrastructure): $224,329 (2014-2017) National Science Foundation (Software and Hardware Foundations): $236,744 (2014-2018) National Science Foundation: $412,261 (2011-2014) National Science Foundation: $91,867 (2008-2012) Dr. Fluet actively mentors graduate students, currently advising several MS project and thesis students. He teaches courses including Programming Skills (with focus on Rust), Compiler Construction, and Programming Language Concepts. He also serves in leadership roles including as Graduate Program Director for the Computer Science MS program and participates in departmental governance through the CS Curriculum Committee and GCCIS Curriculum Committee. He is an active member of the programming languages community, having served on program committees for major conferences and as Information Director for ACM SIGPLAN (2015-2018), demonstrating his commitment to advancing the field through research, education, and community service.
