Find Academic Supervisors

Jeremy GibbonsView profile

Professor

• Functional Programming
• Programming Languages
• Software Engineering
• +3 more

Jeremy Gibbons is a Professor of Computing at the University of Oxford, affiliated with the Department of Computer Science within the Faculty of Computer Science. He serves as Director of the Professional Programmes, overseeing part-time postgraduate degrees in Software Engineering. His roles include Chair of the Faculty of Computer Science (2012–2016), Director of the Software Engineering Programme, and Fellow of Kellogg College. Gibbons' research focuses on programming methodologies, particularly functional and object-oriented languages, with an emphasis on program calculation, design patterns, and bidirectional transformations. He leads the Algebra of Programming research group and is Editor-in-Chief of the Journal of Functional Programming and The Art, Science, and Engineering of Programming . Education includes a D.Phil. from Oxford University. His work spans formal methods, domain-specific modeling for clinical trials (e.g., CancerGrid project), and semantic frameworks for software systems. He has advised numerous students and contributed to open-access initiatives in publishing. Key collaborations include roles in ACM SIGPLAN and IFIP Working Groups 2.1 and 2.11. Research interests emphasize foundational aspects like profunctor optics, categorical programming, and algorithm design. Notable projects include datatype-generic programming and metadata-driven engineering for clinical trials. His work bridges theoretical computer science with practical applications in software architecture and system design.

• Theorem Proving
• Automated Reasoning
• Formal Methods
• +14 more

Jasmin Blanchette is a Professor of Theoretical Computer Science and Theorem Proving at the Institute for Informatics, Ludwig-Maximilians-Universität München (LMU), where he also serves as Dean of Studies for Computer Science since January 2024. He is additionally affiliated as a guest researcher with the VeriDis group at Loria in Nancy, France. His research lies at the intersection of automated and interactive theorem proving, with a focus on higher-order logic and proof automation. Key projects include the development of tools like Sledgehammer, Nitpick, and Zipperposition, and foundational work on (co)datatypes and higher-order superposition. His recent publications reflect a strong trend in formalizing and verifying automated reasoning techniques, especially in higher-order logic, with applications in proof automation, SMT solving, and logical verification. Articles frequently appear in top venues such as CADE, ITP, and the Journal of Automated Reasoning. CADE 2023 Best Paper Award for 'Verified given clause procedures' FroCoS 2023 Best Paper Award (with Visa Nummelin and Sander Dahmen) IPA Dissertation Award (awarded to his student Petar Vukmirović) Dutch 'cum laude' distinction (awarded to his student Anne Baanen) Dutch Prize for ICT Research 2022 Blanchette has advised numerous PhD and postdoctoral researchers, many of whom are now active contributors to the formal methods community. He has received significant research grants through projects like Matryoshka and Nekoka. He is also the editor-in-chief of the Journal of Automated Reasoning and plays a central role in organizing key conferences such as ITP, CADE, and CPP. He leads an active research group at LMU, consisting of postdocs and PhD students working on topics such as higher-order superposition, formalization of voting systems, categorical logic, and proof search heuristics. The team collaborates closely with international groups, including those at Inria and TU Wien.

Nikolaos PapaspyrouView profile

Professor

• Programming Languages
• Software Engineering
• Formal Verification
• +4 more

Nikolaos Papaspyrou is a Professor at the School of Electrical and Computer Engineering of the National Technical University of Athens (NTUA) and a member of the Software Engineering Laboratory . His research focuses on the theory and implementation of programming languages, including semantics, type systems, compilers, static analysis, and formal verification. Since October 2021, he has been on leave from NTUA, working as a Software Engineer for Google in the memory management team for the V8 JavaScript and WebAssembly engine. He previously served as Director of the Division of Computer Science (2017-2019) and was on sabbatical with Google's compiler group in Munich (2015-2016). His work includes the RELEASE project (EU FP7 STREP) for reliable large-scale server software and uncertainty handling in distributed databases (European Social Fund). Ph.D. and Diploma in Electrical and Computer Engineering from NTUA M.Sc. in Computer Science from Cornell University His research interests span programming languages , software engineering , and formal verification , with recent publications on coinductive proofs in Liquid Haskell, concurrency semantics, and quantum compilation. He has supervised over 50 diploma projects and mentored numerous students now at institutions like MIT, Princeton, and UC Berkeley. Awards include conference organizing and program committee roles, though no formal scientific prizes are listed.

Amin TimanyView profile

Associate Professor

• Programming Languages
• Type Theory
• Logical Relations
• +9 more

Amin Timany is an Associate Professor in the Department of Computer Science at Aarhus University, Denmark, where he conducts research in programming languages, type theory, and formal verification. He is a member of the Logic and Semantics Group and actively contributes to the development of logical relations, separation logic, and proof assistants such as Coq and Iris. He holds a PhD in Computer Science from KU Leuven (2018) and was previously a postdoctoral fellow with FWO at KU Leuven. His research focuses on mechanized semantics, program equivalence, concurrency, and distributed systems verification. He is particularly known for solving the long-standing problem of proving encapsulation in the ST monad using logical relations. His recent publications span top-tier venues including POPL, ICFP, PLDI, and CPP, with key contributions in guarded interaction trees, higher-order separation logic (e.g., Trillium), and modular verification of CRDTs and virtual machines. His work emphasizes formalization and mechanization in Coq, often within the Iris framework. He has served on numerous program committees and has chaired conferences such as CPP and sessions at CoqPL. Notably, his paper 'Modular Denotational Semantics for Effects with Guarded Interaction Trees' received a Distinguished Paper Award at POPL 2024. PhD, KU Leuven, 2018 MSc, TU Dresden, 2013 He teaches courses such as Compilation, Program Logics, and Advanced Topics in Programming Language Theory. He collaborates extensively with researchers like Lars Birkedal, Robbert Krebbers, and Derek Dreyer, and mentors students in formal methods and PL theory.

Elena ZuccaView profile

Associate Professor

• Programming Languages
• Type Systems
• Formal Semantics
• +6 more

Elena Zucca is an Associate Professor in the Department of Computer Science, Bioengineering, Robotics and Systems Engineering (DIBRIS) at the University of Genoa, Italy. She has a strong research focus on programming languages, particularly in the areas of type systems, formal semantics, and coinduction. Her work bridges theoretical foundations with practical implementations, as evidenced by her publications on topics like Featherweight Java, corecursion, and soundness proofs for programming language features. Her research interests span the theoretical and practical aspects of programming languages. She investigates the formal semantics of programming constructs, particularly focusing on the boundaries between finite and infinite computations. Her work on coinduction and corecursion explores how to safely handle infinite data structures and computations. She has made significant contributions to understanding soundness in programming language features, especially in relation to resource-aware semantics. Her research often combines theoretical foundations with practical implementations, as seen in her work on Featherweight Java extensions and effect systems. Analysis of her recent publications reveals a consistent focus on advanced type systems and semantics. Her work explores the theoretical boundaries of programming language features while maintaining practical relevance. A recurring theme is the relationship between finite and infinite computations, with particular attention to soundness guarantees. Her research has evolved from foundational work on lambda calculus and object-oriented programming toward more specialized topics like graded types, coeffects, and resource-aware semantics. Elena Zucca has been actively involved in the programming languages research community, serving on program committees for major conferences including SPLASH, ECOOP, and POPL. She has mentored students through doctoral courses on Declarative Programming and (Co)Induction. Her research has been supported through participation in various academic programs, including the SEPL research program mentioned in her course materials. She teaches a diverse range of courses at the University of Genoa, from undergraduate to doctoral levels. Her teaching portfolio includes Automata Theory and Computability, Algorithms Analysis and Design, Principles and Paradigms of Programming Languages, and specialized doctoral courses on Declarative Programming and (Co)Induction. Her courses often reflect her research interests, covering theoretical foundations of programming languages, formal methods, and advanced programming paradigms.

Benjamin C. PierceView profile

Professor

• Programming Languages
• Type Systems
• Language-based Security
• +5 more

Benjamin C. Pierce is the Henry Salvatori Professor of Computer and Information Science in the School of Engineering and Applied Science at the University of Pennsylvania. As a Fellow of the ACM, he has made significant contributions to programming language theory and formal methods. His academic leadership includes previous editorial roles as co-Editor in Chief of the Journal of Functional Programming and Managing Editor for Logical Methods in Computer Science. His research spans multiple interconnected domains in programming language theory, with particular emphasis on type systems and their applications to security and verification. Pierce's work bridges theoretical foundations with practical implementations, most notably through his development of the Unison file synchronization tool and contributions to the Clowdr virtual conference platform. His research interests form a cohesive trajectory from foundational type theory to applied security and verification techniques. Pierce's scholarly output shows consistent focus on property-based testing, type systems, and formal verification methods. His recent publications demonstrate evolving interests in differential privacy verification, synchronization technologies, and the practical challenges of implementing formal methods in real-world systems. The progression of his work reflects both theoretical depth and practical relevance to software development challenges. Fellow of the ACM Author of influential textbooks Types and Programming Languages and Software Foundations Lead designer of the Unison file synchronizer Co-developer of the Clowdr virtual conference platform Former editorial leadership for multiple prominent programming languages journals As an educator and mentor, Pierce has contributed to the Programming Languages Mentoring Workshop (PLMW) and has served on numerous conference program committees. His academic service extends to SIGPLAN leadership roles including SIGPLAN Vice Chair and Steering Committee membership. His textbook Software Foundations has become a standard resource for teaching formal methods and proof assistants.

Peng FuView profile

Assistant Professor

• Type theories
• Quantum programming languages
• Categorical semantics
• +3 more

Peng Fu is an Assistant Professor in the Department of Computer Science and Engineering at the Molinaroli College of Engineering and Computing, University of South Carolina. His academic career focuses on the theoretical foundations of programming languages with particular emphasis on quantum computing applications. Dr. Fu received his educational training from prestigious institutions: Ph.D. in Computer Science from University of Iowa (2014) B.Eng. in Computer Science from Huazhong University of Science and Technology (2009) Dr. Fu's research program centers around type theories, quantum programming languages, and their categorical semantics . His work bridges the gap between theoretical computer science and practical quantum computing applications. He develops formal systems that enable reliable quantum circuit programming through strong type systems and categorical models. His research has significant implications for the future of quantum software development, where correctness and reliability are paramount due to the fragile nature of quantum states. An analysis of Dr. Fu's publication record reveals a consistent trajectory toward increasingly sophisticated quantum programming frameworks. Starting with foundational work on lambda encodings and type theory, he has progressively focused on quantum-specific challenges. His recent papers on Proto-Quipper variants demonstrate innovative approaches to quantum circuit programming with features like dynamic lifting, reversing, and control structures. The research shows strong integration of category theory with practical programming language design, creating bridges between abstract mathematical structures and executable quantum code. Dr. Fu actively mentors the next generation of computer scientists, currently seeking Ph.D. students to join his research group. His teaching portfolio includes advanced courses such as CSCE 790: Quantum Programming Languages (Spring 2025) and CSCE 544: Functional Programming (Fall 2024), where he introduces students to cutting-edge concepts in programming language theory and quantum computing. His commitment to education extends to developing comprehensive course materials and providing guidance to graduate students pursuing research in quantum programming languages. Dr. Fu maintains an active presence in the quantum computing research community, regularly presenting at major conferences including the International Conference on Quantum Physics and Logic (QPL), ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), and specialized quantum computing workshops. His work contributes to the growing ecosystem of quantum programming tools and methodologies that will be essential for practical quantum computing applications.

• Type Theory
• Programming Language Semantics
• Formalization of Mathematics
• +7 more

Niccolò Veltri is an Assistant Professor in the Department of Software Science at Tallinn University of Technology, Estonia. He is a member of the Logic and Semantics research group and co-organizes the Theory Seminar (TSEM). His primary research interests lie in Type Theory , Programming Language Semantics , Formalization of Mathematics , and Categorical Proof Theory . His work emphasizes rigorous formalization using proof assistants, particularly Agda, to develop and verify complex logical and computational systems. The recent publications highlight a consistent focus on foundational aspects of logic and computation. Key themes include the formalization and metatheory of substructural and non-commutative logics (e.g., Lambek calculus, skew monoidal categories), the use of focusing for proof normalization, the semantics of process calculi (CCS, π-calculus) in guarded and cubical type theories, and the constructive treatment of coinductive data and final semantics. The consistent use of Agda for formalization is a hallmark of his research output. No scientific awards were mentioned in the provided text. Niccolò Veltri advises several PhD students, including Michel Smykalla, Ioannis Andreou, Andrea Laretto, Michele De Pascalis, Philipp Joram, and Cheng-Syuan Wan, often in collaboration with Tarmo Uustalu and Fosco Loregian. There is no mention of specific grants in the provided text. He is a core member of the Logic and Semantics research group at the Institute of Computer Science, Tallinn University of Technology, which drives his collaborative research and the organization of the Theory Seminar (TSEM).

Rodolphe LepigreView profile

Researcher

• Formal Methods
• Programming Languages
• Type Systems
• +3 more

Rodolphe Lepigre is a researcher in computer science affiliated with the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, Germany, within Derek Dreyer's group. He holds a Researcher academic rank. His work focuses on formal methods, programming languages, and type systems. Previously, he was a postdoctoral researcher at Inria (Deducteam project) and completed his PhD at Université Savoie Mont Blanc in the LAMA laboratory. Research Interests: His research spans formal verification of concurrent systems, separation logic, proof assistants, and the integration of program certification within ML-style languages. He has contributed to projects like PML₂ and RefinedC, aiming to bridge practical programming with formal guarantees. Key Contributions: His work includes the VIP framework for verifying C idioms, extensions to separation logic with prophecy variables, and foundational type systems for Curry-style languages. He has also developed tools like the Dedukti logical framework and the Bindlib library for OCaml. Awards: Recipient of the PLDI 2021 Distinguished Paper and Artifact Awards for contributions to C code verification. His work on RefinedC highlights advancements in automated verification tools. Grants & Collaborations: Collaborations include projects with Inria, MPI-SWS, and contributions to open-source tools like the PML₂ language and the Lambdapi proof assistant. His research is supported by grants from European and German research institutions.

Elsa GunterView profile

Research Professor

• Formal methods
• programming languages
• software engineering
• +6 more

Elsa Gunter is a Research Professor at the Department of Computer Science , University of Illinois at Urbana-Champaign . Her work bridges formal methods , programming languages , and human-computer interaction with a focus on verification and security. Education: Ph.D. in Mathematics, University of Wisconsin-Madison (1987) M.A. in Mathematics, University of Wisconsin-Madison (1981) B.A. in Mathematics, University of Chicago (1979) Her research interests include formal verification , type theory , and secure system design . She has developed tools like VeriF-OPT for parallel program optimization and Tutela for modeling human-computer protection envelopes. Her recent publications focus on concurrent systems , compiler verification , and security protocols . Notable awards include the Most Influential 10-Year Paper Award at RE 2010 and the EASST Best Paper at ETAPS 2001 . She has advised students like Dennis Griffith and Liyi Li , while collaborating on projects such as DSILL (distributed functional language) and PTRANS (program transformation semantics).

Paul DownenView profile

Assistant Professor

• Programming Languages
• Logic
• Type Theory
• +4 more

Paul Downen is an Assistant Professor at the Miner School of Computer & Information Sciences, University of Massachusetts, Lowell, since Fall 2021. He holds a Ph.D. in Computer and Information Science from the University of Oregon (2017). His research bridges programming languages, logic, type theory, and compiler design, emphasizing computational duality and verification. Focus areas: Sequent calculus as a compiler intermediate language Development of Sequent Core and Join Points for GHC optimization Advocacy for functional programming in high-assurance systems His work spans both theoretical foundations and practical implementations, including contributions to Haskell compilers and the design of educational materials for programming language theory. He has received a Best Paper Award at PLDI 2017 and a Best Paper Award nomination at TFP 2025. Recent publications examine the intersection of logic and programming language design, with specific emphasis on contextual reasoning, structural coinduction, and efficient compilation techniques. He has taught courses on functional programming, logic and verification, and assembly language at UMass Lowell.

• Topology
• Category Theory
• Computer Science
• +4 more

Dr. Paige North is an Assistant Professor at Utrecht University, holding a dual appointment in the Department of Mathematics and the Department of Information and Computing Sciences . She combines topology and category theory to address challenges in computer science, particularly focusing on the interplay between functional programming/type theory and homotopy theory/higher category theory . Her research includes formalizing double categories, model category theory, and dependent type theories within univalent foundations. She has taught courses like Homotopy Type Theory and Advanced Functional Programming, and actively participates in organizing academic events such as the UniMath School and DutchCATS Workshop . Funding: AFOSR grant (2021–2024) Awards: Honorary Research Fellow, University of Birmingham Key Collaborations: Nima Rasekh, Benedikt Ahrens, Michael Shulman

Zena M. AriolaView profile

Researcher

• Programming Languages
• Theoretical Computer Science
• Functional Programming
• +3 more

Zena M. Ariola is affiliated with the University of Oregon, USA, and has actively participated in academic leadership roles across programming language conferences. She has served as Program Chair and Committee Member for ICFP, PEPM, and PLDI, while contributing to research in compiler design, type theory, and formal methods. Active in POPL, ICFP, PLDI, and other premier programming language conferences Focus on theoretical foundations of programming languages and compiler design Contributions include advancements in sequent calculus, coinduction, and closure conversion Her research spans programming language semantics, formal verification, and efficient execution models. She has authored key publications in these areas and contributed to academic governance through committee memberships and chair roles. Recent publications examine formal methods for compiler intermediate languages, structural coinduction, and closure conversion techniques. These works intersect with subfields such as type theory, functional programming, and control flow optimization. While no specific awards are listed in the provided materials, her extensive publication record and leadership roles demonstrate significant academic contributions. Zena Ariola's work connects programming language theory with practical implementation challenges, influencing both academic research and compiler development practices.

Maximilien PérouxView profile

Visiting Assistant Professor

• Algebraic Topology
• Stable Homotopy Theory
• Algebraic K-theory
• +3 more

Maximilien Péroux is a Visiting Assistant Professor in the Department of Mathematics at Michigan State University (MSU). His postdoctoral mentor at MSU is Teena Gerhardt. Previously, he was a postdoc at the University of Pennsylvania (2020-2023), mentored by Mona Merling, and completed his PhD at the University of Illinois at Chicago (2015-2020), advised by Brooke Shipley. He holds a Master’s and Bachelor’s from École Polytechnique Fédérale de Lausanne (EPFL), with a visiting research period at MIT (2014) under Haynes Miller. Education: PhD in Mathematics (2015-2020), University of Illinois at Chicago, advised by Brooke Shipley. Master’s in Fundamental Mathematics (2013-2015), EPFL, advised by Kathryn Hess. Bachelor’s in Mathematics (2010-2013), EPFL. Visiting Research at MIT (Fall 2014), advised by Haynes Miller and Kathryn Hess. His research focuses on Algebraic Topology, Stable Homotopy Theory, Algebraic K-theory, and Higher Category Theory, with additional interests in Theoretical Computer Science. He explores coalgebraic structures, homotopy theory applications, and categorical frameworks, integrating methods from algebraic topology into foundational computer science problems. Péroux’s recent publications (2018–2025) emphasize coalgebraic structures, homotopy theory, and categorical methods. Key themes include coHochschild homology, Koszul duality in higher topoi, and monoidal Dold-Kan correspondences. His work bridges algebraic topology with theoretical computer science through enriched data types and coinductive control mechanisms. His advising and mentorship include collaborations with Teena Gerhardt (MSU), Mona Merling (UPenn), and Brooke Shipley (UIC). No specific grants are listed, though his postdoctoral positions reflect institutional support.

Graham HuttonView profile

Professor

• Mathematics of program construction
• Functional programming
• Programming language semantics
• +6 more

Graham Hutton is a Professor of Computer Science at the University of Nottingham , where he leads the Functional Programming Lab and serves as Director of the Midlands Graduate School . He co-founded the Quotient Haskell project and maintains key roles in Journal of Functional Programming editorial work and Haskell Foundation governance. Co-leader, Functional Programming Lab (2008–date) Director, Midlands Graduate School (2023–date) ACM Distinguished Scientist Principal investigator for £912k EPSRC project (2024–2027) His research focuses on mathematical approaches to program construction , particularly through functional languages like Haskell and Agda . He develops techniques for compiler correctness , type system design , and program optimization , with recent work on quotient polymorphism and denotational cost models . Key article themes include: Compiler derivation from formal semantics Effect handling in functional languages Graph-based code generation over traditional tree structures Quotient type systems with SMT solver integration Concurrency semantics using choice trees Operational improvement with parametric polymorphism Scientific awards include: ACM Distinguished Scientist (2013) Best Paper & Best Student Paper (2018) EPSRC funding for compiler correctness projects He advises current PhD students in compiler calculation and memory safety , while maintaining extensive educational contributions through his widely-used textbook Programming in Haskell and open course materials.