Find Academic Supervisors

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.

• Functional Programming
• Programming Languages
• Software Engineering
• +3 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.

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

Andrei Popescu is a Senior Lecturer in Computing Foundations at the School of Computer Science, University of Sheffield, where he also serves as School Programmes Lead (PGT). He is a member of both the Security of Advanced Systems research group and the Foundations of Computation research group. Prior to joining Sheffield in May 2020, he was a Lecturer at Middlesex University and a postdoctoral researcher at TU Munich. Dr. Popescu holds dual PhDs: one in computer science from the University of Illinois at Urbana-Champaign (advised by Elsa L. Gunter and Grigore Roșu) and another in mathematics from the University of Bucharest (advised by George Georgescu). His primary research interests include proof assistants, information flow security, inductive and coinductive datatypes, automated deduction, and syntax with bindings. His work often focuses on the formal verification of security properties in practical systems, as evidenced by projects like CoCon (a conference management system with verified confidentiality) and CoSMeDis (a social media platform with formally verified security guarantees). Analysis of his recent publications reveals a strong focus on foundational aspects of proof assistants, particularly Isabelle/HOL, with significant contributions to syntax with bindings, recursion principles, and the formalization of Gödel's incompleteness theorems. His work bridges theoretical computer science with practical applications in security verification. Scientific Awards: Distinguished paper award at POPL 2025 for 'Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings' Distinguished paper award at POPL 2024 for 'Nominal Recursors as Epi-Recursors' Distinguished paper award at POPL 2023 for 'Admissible Types-to-PERs Relativization in Higher-Order Logic' Dr. Popescu has successfully supervised PhD students, including Lorenzo Gheri whose thesis focused on syntax with bindings. He has secured significant research funding, including the COVERT project (EPSRC, £422,585), Security of Digital Twins in Manufacturing (EPSRC, £774,954), and Cyclic Reasoning Mechanisms for Interactive Theorem Proving (Royal Society, £12,000). He is actively involved in the research community, serving on program committees for major conferences including POPL, ITP, CSF, and IJCAR, and co-organizing the Midlands Graduate School. His work with the Security of Advanced Systems group continues to advance the field of formal verification for security-critical systems.

• Proof assistants
• Information flow security
• Inductive and coinductive datatypes
• +5 more

Asta Halkjær From is a postdoctoral researcher in the Department of Computer Science at the University of Copenhagen, affiliated with the Software, Data, People & Society (SDPS) section under Dmitriy Traytel. She previously completed her PhD at DTU Compute from 2020 to 2023, focusing on formalized deduction methods in computational logic. She holds a Master’s and Bachelor’s degree from DTU in Computer Science and Software Technology, respectively, with a specialization in Artificial Intelligence and Algorithms. Her research lies at the intersection of formal logic and computer science, particularly in automated reasoning, proof assistants (Isabelle/HOL and Lean), and mechanized metatheory. She has contributed extensively to synthetic completeness proofs, tableau systems, and verified theorem provers. Her work emphasizes formal verification of logical systems, including epistemic logic, hybrid logic, and first-order logic, with a focus on soundness and completeness. The recent publications highlight a consistent trend: the mechanization of logical foundations in proof assistants. Her work bridges theoretical logic with practical verification tools, enabling reliable automation in theorem proving. She has developed and verified provers, explored axiomatic systems, and advanced the methodology of synthetic completeness, often leveraging Isabelle/HOL’s framework. Distinguished Paper Award, CPP 2023 DTU Young Researcher Award DTU Travel Grant (Executive Board Recognition) Otto Mønsted Fonden Travel Grant She has supervised BSc and MSc theses, special courses, and research projects at DTU, and currently teaches Software Development for Digital Health . She has served on program committees for CPP, ITP, and Dalí workshops and has reviewed for journals including Journal of Automated Reasoning and Journal of Logic and Computation . She has also participated in international research visits, including at VU Amsterdam. She is actively involved in building tools for formal reasoning and maintains a personal website with resources, including an Isabelle snippets generator and bibliography tools. Her work continues to advance the foundations of formal logic through mechanized proofs and practical automation.

• Formal Logic
• Automated Reasoning
• Theorem Proving
• +13 more

Henning Basold is affiliated with ENS Lyon , where he contributes as a Researcher . His work centers on theoretical computer science, particularly coinductive logic and corecursive proof search in programming languages and formal methods. In 2019, he authored two pivotal publications at ETAPS 2019 conferences: Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses (ESOP 2019) Coinduction in Uniform: what's next? (HCVS 2019) These works explore coinductive techniques, Horn clauses, and future directions in formal verification and proof theory.

• Computer Science
• Logic in Computer Science
• Programming Languages
• +2 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.

• Programming Languages
• Software Engineering
• Formal Verification
• +4 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.

• Programming Languages
• Type Theory
• Logical Relations
• +9 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.

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

Andreas Abel is a Senior Lecturer at the Department of Computer Science, Gothenburg University, with a focus on Programming Languages, Logic, and Type Theory. His work includes contributions to dependently typed programming, functional programming, lambda calculus, and formal verification. Research Interests Programming Languages Logic Types Projects Principal Investigator for Modal Dependent Type Theory (Vetenskapsrådet grant 2020-2024) Editor of the Theoretical Pearls column in the Journal of Functional Programming Senior developer of the dependently-typed language Agda His recent publications span graded type theory, normalization by evaluation, strong normalization, and formal verification using Agda. Key collaborations include Jean-Philippe Bernardy and Thierry Coquand. Scientific Awards Vetenskapsrådet grant 2020-2024 VR Grant 2014-04864 He has supervised numerous projects, developed software tools like the Backus Naur Form Compiler (BNFC), and contributed to international conferences as a PC member and author.

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

Brigitte Pientka is a Full Professor in the School of Computer Science at McGill University, leading the Computation and Logic research group. She holds a PhD from Carnegie Mellon University (2003) and has conducted studies at the University of Edinburgh and Technical University of Darmstadt. Her research focuses on theoretical foundations of reliable software systems, combining programming languages, type theory, and theorem proving. Notable contributions include work on modal dependent type theory, contextual types, and mechanizing meta-theoretic proofs using the Beluga system. Her academic roles include serving as General Chair of POPL 2020, Program Chair for ICFP 2024 and CPP 2023/2024, and Executive Editor of Logical Methods in Computer Science. Awards include the Humboldt Fellowship and a Test of Time Award at PPDP'18. She actively contributes to conference PCs and editorial boards, emphasizing formal methods and programming languages. Pientka teaches advanced courses on programming languages (COMP 523, COMP 527), logic, and dependently typed systems (COMP 599, COMP 762). Her work spans theoretical advancements and practical tools, with a focus on educating students in functional programming and formal verification. She advocates for diversity in computer science, encouraging underrepresented groups to pursue research opportunities.

• Programming Languages
• Type Theory
• Theorem Proving
• +6 more

Nikolaos S. Papaspyrou is a Professor at the School of Electrical and Computer Engineering of the National Technical University of Athens (NTUA), affiliated with the Software Engineering Laboratory and the Division of Computer Science. His research focuses on programming languages, compilers, formal verification, and concurrency. Since October 2021, he has been on leave from NTUA while working as a Software Engineer at Google's V8 JavaScript and WebAssembly engine team. Previously, he served as Director of the Division of Computer Science (2017–2019) and held a sabbatical at Google's Munich compiler group (2015–2016). His academic contributions include pioneering work on Erlang/OTP scalability, concolic testing for functional languages, and static analysis techniques. He has authored numerous publications in top venues like ACM Transactions on Programming Languages and Systems and IEEE conferences. Papaspyrou has supervised over 50 diploma students and multiple PhD candidates, contributing to the education of future researchers and engineers. He actively participates in programming competitions, coaching Greek Olympiad teams, and volunteers in the Hellenic Informatics Society. He teaches advanced courses on programming languages, compilers, and software engineering at NTUA, emphasizing practical applications of theoretical concepts. His educational philosophy integrates problem-solving through programming, as highlighted in his FedCSIS 2013 paper on teaching methodologies.

• Programming Languages
• Semantics
• Type Systems
• +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.

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

Andreas Abel is a Senior Lecturer in the Department of Computer Science and Engineering at Gothenburg University, with additional affiliation at Chalmers University of Technology. He is a senior developer of the Agda programming language and maintains the Backus Naur Form Compiler (BNFC). His educational background includes a Computer Science diploma (1999), PhD (2006), and Habilitation (2013), all from Ludwig-Maximilians-University (LMU) Munich. His career spans positions at LMU, INRIA Paris, and Chalmers before his current role at Gothenburg University since 2013. Abel's research focuses on dependently typed programming , type theory , and verified software development . His work bridges theoretical foundations with practical implementations, particularly in the Agda proof assistant. His interests span from foundational aspects of lambda calculus and normalization to practical applications in programming language design. His publications demonstrate a consistent focus on type theory foundations and practical implementations, with recent work exploring applicative functors, cubical type theory, modalities in type systems, and formalizations of algebraic structures. His research often combines deep theoretical insights with concrete implementations in proof assistants. Distinguished Paper Award at ICFP 2019 (4 out of 39 accepted papers) Editor of Theoretical Pearls column, Journal of Functional Programming Member of IFIP WG 1.3 on Foundations of System Specification Abel actively supervises students through the Initial Types Club and Master's thesis projects, focusing on advanced topics in programming languages and type theory. He teaches Programming Language Technology and Advanced Functional Programming, emphasizing both theoretical foundations and practical implementation. His current research is supported by a Vetenskapsrådet grant for the project 'Modal Dependent Type Theory' (2020-2024), continuing his long-standing contributions to programming language theory and formal verification.

• Type Theory
• Dependent Types
• Programming Languages
• +7 more

Andrei Popescu is a Senior Lecturer (Associate Professor level) in the Department of Computer Science at the University of Sheffield, where he conducts research in formal methods, proof assistants, and information flow security. He previously held academic positions at Middlesex University and TU Munich. University: University of Sheffield Department: Department of Computer Science Previous Affiliations: Middlesex University, TU Munich His research focuses on the logical foundations and practical applications of proof assistants, particularly Isabelle/HOL. He has made foundational contributions to inductive and coinductive datatypes, syntax with bindings, higher-order logic, and the formal verification of secure systems. His work bridges theoretical logic with real-world systems such as conference management (CoCon) and social media platforms (CoSMeDis). The recent publications highlight a strong trend in formalizing deep logical results (e.g., Gödel’s incompleteness theorems), advancing datatype theory, verifying complex security properties, and applying formal methods to practical systems. His work consistently appears in top-tier venues such as POPL, CAV, ITP, and CSF. Distinguished Paper Award at POPL 2025 Distinguished Paper Award at POPL 2024 Distinguished Paper Award at POPL 2023 RS 3 Best Paper Award for 2012–2013 He has advised PhD students including Lorenzo Gheri and has been actively involved in organizing major academic events such as the Midlands Graduate School, CPP, ITP, and TABLEAUX conferences. He has served on numerous program committees including POPL, ITP, CSF, and CAV, and has led research projects funded by VeTSS and industrial partners. He is a key contributor to the Isabelle proof assistant ecosystem, particularly in the development of the (co)datatype package and foundational consistency results. His work combines deep theoretical insight with practical implementation, making significant impacts in both academia and applied security.

• Proof Assistants
• Formal Verification
• Inductive and Coinductive Datatypes
• +12 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).

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