معرفی
Christine Rizkallah is a Senior Lecturer in the School of Computing and Information Systems at the University of Melbourne, Australia. She joined the university in December 2021 after serving as a Lecturer at the University of New South Wales (UNSW) from April 2018 to December 2021. Her research focuses on interactive theorem proving, formal verification, programming languages, and systems, with an emphasis on building practical tools for high-assurance software development. She leads a research group working on the Cogent and Dargent languages, aiming to reduce the burden of formal verification in systems programming.
Education:
- PhD in Computer Science, Universität des Saarlandes and Max-Planck-Institut für Informatik, Germany (2015), thesis: Verification of Program Computations, supervised by Prof. Dr. Kurt Mehlhorn.
- MSc in Computer Science, Universität des Saarlandes, Germany (2009), thesis: Proof Representations for Higher Order Logic, supervised by Prof. Dr. Gert Smolka and Dr. Chad E. Brown.
- BSc in Computer Science, German University in Cairo, Egypt (2007), thesis: X2-Planner: A Hierarchical Task Network Planner for Real Time Gaming Applications, supervised by Prof. Dr. Slim Abdennadher and Dr. Thorsten Maier.
Her research interests lie at the intersection of programming languages and formal methods. She develops domain-specific languages with strong type systems and verified compilers to enable trustworthy software systems. Her work spans algorithms, logic, security, and social choice theory, reflecting a strong interdisciplinary approach. She has published extensively in top venues such as POPL, ICFP, ASPLOS, JAR, and PACMPL, with a focus on certifying compilation, refinement verification, and mechanized reasoning.
Her recent publications reveal a consistent focus on formal verification of systems software, particularly through the Cogent language and its ecosystem. Key themes include verified data layout refinement (Dargent), property-based testing, termination analysis, cost modeling, and integration with foreign functions. Her work combines theoretical rigor with practical implementation, often involving mechanized proofs in Isabelle/HOL and Coq.
Scientific Awards and Recognition:
- Distinguished Artefact Award at SLE'22 (awarded to Zilin Chen for work under her supervision).
- First Prize, SPLASH'22 Student Research Competition (undergraduate), won by Raphael Douglas Giles.
- Second Prize, ACM-wide Student Research Competition (undergraduate, 2023), won by Raphael Douglas Giles.
She has supervised numerous PhD, Masters, and Honours students, many of whom have continued in academia or industry research roles. She has received research funding through institutional support and collaborative grants, though specific grants are not detailed in the provided text. She is actively involved in the programming languages community, serving on program committees for POPL, ICFP, CPP, PLDI, and others, and holding leadership roles such as Program Chair for FUNARCH'25 and Diversity and Inclusion Co-Chair for PLDI'25. She teaches core courses including Declarative Programming and Models of Computation at the University of Melbourne.
She leads a vibrant research team and collaborates widely across institutions including UNSW, University of Pennsylvania, and international partners. Her lab focuses on building verified systems using functional programming and formal methods, with strong ties to the DeepSpec project and the Isabelle/HOL community.
