Christine Rizkallah

48 papers A* 4A 2B 11C 1Journal 25Unranked 4
YearRankTypeTitle / Venue / Authors
2026 — conf
The Memorist Tale: Every Thunk Every Cost All At Once.
ESOP (1)
Xing Li, Yao Li, Peter Schachte, Christine Rizkallah
2026 J jnl
Uniqueness is Separation.
CoRR
Liam O'Connor, Pilar Selene Linares-Arévalo, Christine Rizkallah
2025 B conf
A Verified Cost Model for Call-By-Push-Value.
ITP
Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah
2025 J jnl
Formalised Burrows-Wheeler Transform.
Arch. Formal Proofs
Louis Cheung, Christine Rizkallah
2025 C conf
Formalising Fairness in the Assignment Problem with Ordinal Preferences in Isabelle/HOL.
CICM
Duc Minh Do, Christine Rizkallah
2025 B conf
Formalized Burrows-Wheeler Transform.
CPP
Louis Cheung, Alistair Moffat, Christine Rizkallah
2025 J jnl
Formally Verified Suffix Array Construction.
J. Autom. Reason.
Louis Cheung, Alistair Moffat, Christine Rizkallah
2025 J jnl
From Empirical Evaluation to Context-Aware Enhancement: Repairing Regression Errors with LLMs.
CoRR
Anh Ho, Thanh Le-Cong, Bach Le, Christine Rizkallah
2025 B conf
Memory Safety: Uniqueness as Separation.
APLAS
Pilar Selene Linares-Arévalo, Arthur Azevedo de Amorim, Vincent Jackson, Liam O'Connor, Peter Schachte, Christine Rizkallah
2024 B conf
A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras.
ITP
Vincent Jackson, Toby Murray, Christine Rizkallah
2024 J jnl
Formally Verified Suffix Array Construction.
Arch. Formal Proofs
Louis Cheung, Christine Rizkallah
2024 A* conf
T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations.
ICALP
Raphael Douglas Giles, Vincent Jackson, Christine Rizkallah
2023 J jnl
Dargent: A Silver Bullet for Verified Data Layout Refinement.
Proc. ACM Program. Lang.
Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, Christine Rizkallah
2022 B conf
Overcoming restraint: composing verification of foreign functions with cogent.
CPP
Louis Cheung, Liam O'Connor, Christine Rizkallah
2022 B conf
Property-Based Testing: Climbing the Stairway to Verification.
SLE
Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, Gabriele Keller
2021 J jnl
Cogent: uniqueness types and certifying compilation.
J. Funct. Program.
Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele Keller
2021 J jnl
Overcoming Restraint: Modular Refinement using Cogent's Principled Foreign Function Interface.
CoRR
Louis Cheung, Liam O'Connor, Christine Rizkallah
2021 J jnl
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code.
J. Funct. Program.
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua M. Cohen, Stephanie Weirich
2018 B conf
A Formal Equational Theory for Call-By-Push-Value.
ITP
Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic
2018 — conf
Bringing Effortless Refinement of Data Layouts to Cogent.
ISoLA (1)
Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah, Gerwin Klein, Gabriele Keller
2018 A* conf
Rank Maximal Equal Contribution: A Probabilistic Social Choice Function.
AAAI
Haris Aziz, Pang Luo, Christine Rizkallah
2018 J jnl
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code.
CoRR
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich
2018 J jnl
Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report).
Proc. ACM Program. Lang.
Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich
2018 J jnl
Structural Operational Semantics for Control Flow Graph Machines.
CoRR
Dmitri Garbuzov, William Mansky, Christine Rizkallah, Steve Zdancewic
2018 B conf
Total Haskell is reasonable Coq.
CPP
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich
2017 B conf
Complx: a verification framework for concurrent imperative programs.
CPP
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong
2017 J jnl
Rank Maximal Equal Contribution: a Probabilistic Social Choice Function.
CoRR
Haris Aziz, Pang Luo, Christine Rizkallah
2017 J jnl
Total Haskell is Reasonable Coq.
CoRR
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich
2016 J jnl
A Dependent Security Type System for Concurrent Imperative Programs.
Arch. Formal Proofs
Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
2016 B conf
A Framework for the Automatic Formal Verification of Refinement from Cogent to C.
ITP
Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein
2016 J jnl
COGENT: Certified Compilation for a Functional Systems Language.
CoRR
Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein
2016 J jnl
COMPLX: A Verification Framework for Concurrent Imperative Programs.
Arch. Formal Proofs
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong
2016 A* conf
CoGENT: Verifying High-Assurance File System Implementations.
ASPLOS
Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby C. Murray, Gerwin Klein, Gernot Heiser
2016 J jnl
Compositional Security-Preserving Refinement for Concurrent Imperative Programs.
Arch. Formal Proofs
Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
2016 A conf
Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference.
CSF
Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
2016 J jnl
Incompatibility of Efficiency and Strategyproofness in the Random Assignment Setting with Indifferences.
CoRR
Haris Aziz, Pang Luo, Christine Rizkallah
2016 B conf
Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency.
ITP
June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah
2016 A conf
Refinement through restraint: bringing down the cost of verification.
ICFP
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein
2015 — —
Verification of program computations.
Christine Rizkallah
2014 J jnl
A Framework for the Verification of Certifying Computations.
J. Autom. Reason.
Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah
2014 J jnl
Glivenko and Kuroda for Simple Type Theory.
J. Symb. Log.
Chad E. Brown, Christine Rizkallah
2014 — conf
Verification of Certifying Computations through AutoCorres and Simpl.
NASA Formal Methods
Lars Noschinski, Christine Rizkallah, Kurt Mehlhorn
2013 J jnl
A Framework for the Verification of Certifying Computations
CoRR
Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah
2013 J jnl
An Axiomatic Characterization of the Single-Source Shortest Path Problem.
Arch. Formal Proofs
Christine Rizkallah
2013 — conf
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction.
PxTP@CADE
Chad E. Brown, Christine Rizkallah
2011 J jnl
An Introduction to Certifying Algorithms.
it Inf. Technol.
Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah, Pascal Schweitzer
2011 J jnl
Maximum Cardinality Matching.
Arch. Formal Proofs
Christine Rizkallah
2011 A* conf
Verification of Certifying Computations.
CAV
Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, Christine Rizkallah