Pure Type Systems without Explicit Contexts - Herman Geuvers; Robbert Krebbers; James McKinna; Freek Wiedijk (LFMTP, 2010)

Computer Certified Efficient Exact Reals in Coq. - Robbert Krebbers; Bas Spitters (Calculemus/MKM, 2011)

A Formalization of the C99 Standard in HOL, Isabelle and Coq. - Robbert Krebbers; Freek Wiedijk (Calculemus/MKM, 2011)

Type classes for efficient exact real arithmetic in Coq - Robbert Krebbers; Bas Spitters (Log. Methods Comput. Sci., 2011)

The correctness of Newman's typability algorithm and some of its extensions. - Herman Geuvers; Robbert Krebbers (Theor. Comput. Sci., 2011)

The lambda-mu-T-calculus - Herman Geuvers; Robbert Krebbers; James McKinna (CoRR, 2012)

A call-by-value lambda-calculus with lists and control - Robbert Krebbers (CL&C, 2012)

Aliasing Restrictions of C11 Formalized in Coq. - Robbert Krebbers (CPP, 2013)

Separation Logic for Non-local Control Flow and Block Scope Variables. - Robbert Krebbers; Freek Wiedijk (FoSSaCS, 2013)

The λμT-calculus. - Herman Geuvers; Robbert Krebbers; James McKinna (Ann. Pure Appl. Log., 2013)

Formal C Semantics: CompCert and the C Standard. - Robbert Krebbers; Xavier Leroy; Freek Wiedijk (ITP, 2014)

An operational and axiomatic semantics for non-determinism and sequence points in C. - Robbert Krebbers (POPL, 2014)

Separation Algebras for C Verification in Coq. - Robbert Krebbers (VSTTE, 2014)

A Typed C11 Semantics for Interactive Theorem Proving. - Robbert Krebbers; Freek Wiedijk (CPP, 2015)

Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq. - Robbert Krebbers; Louis Parlant; Alexandra Silva 001 (Theory and Practice of Formal Methods, 2016)

Higher-order ghost state. - Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (ICFP, 2016)

A Formal C Memory Model for Separation Logic. - Robbert Krebbers (J. Autom. Reason., 2016)

The Essence of Higher-Order Concurrent Separation Logic. - Robbert Krebbers; Ralf Jung 002; Ales Bizjak; Jacques-Henri Jourdan; Derek Dreyer; Lars Birkedal (ESOP, 2017)

Interactive proofs in higher-order concurrent separation logic. - Robbert Krebbers; Amin Timany; Lars Birkedal (POPL, 2017)

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. - Dan Frumin; Robbert Krebbers; Lars Birkedal (LICS, 2018)

Iris from the ground up: A modular foundation for higher-order concurrent separation logic. - Ralf Jung 002; Robbert Krebbers; Jacques-Henri Jourdan; Ales Bizjak; Lars Birkedal; Derek Dreyer (J. Funct. Program., 2018)

RustBelt: securing the foundations of the rust programming language. - Ralf Jung 002; Jacques-Henri Jourdan; Robbert Krebbers; Derek Dreyer (Proc. ACM Program. Lang., 2018)

Mtac2: typed tactics for backward reasoning in Coq. - Jan-Oliver Kaiser; Beta Ziliani; Robbert Krebbers; Yann Régis-Gianas; Derek Dreyer (Proc. ACM Program. Lang., 2018)

MoSeL: a general, extensible modal framework for interactive proofs in separation logic. - Robbert Krebbers; Jacques-Henri Jourdan; Ralf Jung 002; Joseph Tassarotti; Jan-Oliver Kaiser; Amin Timany; Arthur Charguéraud; Derek Dreyer (Proc. ACM Program. Lang., 2018)

Intrinsically-typed definitional interpreters for imperative languages. - Casper Bach Poulsen; Arjen Rouvoet; Andrew Tolmach; Robbert Krebbers; Eelco Visser (Proc. ACM Program. Lang., 2018)

Semi-automated Reasoning About Non-determinism in C Expressions. - Dan Frumin; Léon Gondelman; Robbert Krebbers (ESOP, 2019)

A benchmark for C program verification. - Marko C. J. D. van Eekelen; Daniil Frumin; Herman Geuvers; Léon Gondelman; Robbert Krebbers; Marc Schoolderman; Sjaak Smetsers; Freek Verbeek; Benoît Viguier; Freek Wiedijk (CoRR, 2019)

Iron: managing obligations in higher-order concurrent separation logic. - Ales Bizjak; Daniel Gratzer; Robbert Krebbers; Lars Birkedal (Proc. ACM Program. Lang., 2019)

Intrinsically-typed definitional interpreters for linear, session-typed languages. - Arjen Rouvoet; Casper Bach Poulsen; Robbert Krebbers; Eelco Visser (CPP, 2020)

Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. - Paolo G. Giarrusso; Léo Stefanesco; Amin Timany; Lars Birkedal; Robbert Krebbers (Proc. ACM Program. Lang., 2020)

Actris: session-type based reasoning in separation logic. - Jonas Kastberg Hinrichsen; Jesper Bengtson; Robbert Krebbers (Proc. ACM Program. Lang., 2020)

Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications. - Arjen Rouvoet; Hendrik van Antwerpen; Casper Bach Poulsen; Robbert Krebbers; Eelco Visser (Proc. ACM Program. Lang., 2020)

Machine-checked semantic session typing. - Jonas Kastberg Hinrichsen; Daniël Louwrink; Robbert Krebbers; Jesper Bengtson (CPP, 2021)

RefinedC: automating the foundational verification of C code with refined ownership types. - Michael Sammler; Rodolphe Lepigre; Robbert Krebbers; Kayvan Memarian; Derek Dreyer; Deepak Garg 001 (PLDI, 2021)

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. - Simon Spies; Lennard Gäher; Daniel Gratzer; Joseph Tassarotti; Robbert Krebbers; Derek Dreyer; Lars Birkedal (PLDI, 2021)

Compositional Non-Interference for Fine-Grained Concurrent Programs. - Dan Frumin; Robbert Krebbers; Lars Birkedal (SP, 2021)

Safe systems programming in Rust. - Ralf Jung 002; Jacques-Henri Jourdan; Robbert Krebbers; Derek Dreyer (Commun. ACM, 2021)

ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. - Dan Frumin; Robbert Krebbers; Lars Birkedal (Log. Methods Comput. Sci., 2021)

Intrinsically typed compilation with nameless labels. - Arjen Rouvoet; Robbert Krebbers; Eelco Visser (Proc. ACM Program. Lang., 2021)

Diaframe: automated verification of fine-grained concurrent programs in Iris. - Ike Mulder; Robbert Krebbers; Herman Geuvers (PLDI, 2022)

Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. - Jonas Kastberg Hinrichsen; Jesper Bengtson; Robbert Krebbers (Log. Methods Comput. Sci., 2022)

Simuliris: a separation logic framework for verifying concurrent program optimizations. - Lennard Gäher; Michael Sammler; Simon Spies; Ralf Jung 002; Hoang-Hai Dang; Robbert Krebbers; Jeehoon Kang; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Connectivity graphs: a method for proving deadlock freedom based on separation logic. - Jules Jacobs; Stephanie Balzer; Robbert Krebbers (Proc. ACM Program. Lang., 2022)

Multiparty GV: functional multiparty session types with certified deadlock freedom. - Jules Jacobs; Stephanie Balzer; Robbert Krebbers (Proc. ACM Program. Lang., 2022)

VIP: verifying real-world C idioms with integer-pointer casts. - Rodolphe Lepigre; Michael Sammler; Kayvan Memarian; Robbert Krebbers; Derek Dreyer; Peter Sewell (Proc. ACM Program. Lang., 2022)

Later credits: resourceful reasoning for the later modality. - Simon Spies; Lennard Gäher; Joseph Tassarotti; Ralf Jung 002; Robbert Krebbers; Lars Birkedal; Derek Dreyer (Proc. ACM Program. Lang., 2022)

Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). - Robbert Krebbers (ITP, 2023)

Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. - Ike Mulder; Lukasz Czajka 001; Robbert Krebbers (Proc. ACM Program. Lang., 2023)

DimSum: A Decentralized Approach to Multi-language Semantics and Verification. - Michael Sammler; Simon Spies; Youngju Song; Emanuele D'Osualdo; Robbert Krebbers; Deepak Garg 001; Derek Dreyer (Proc. ACM Program. Lang., 2023)

Proof Automation for Linearizability in Separation Logic. - Ike Mulder; Robbert Krebbers (Proc. ACM Program. Lang., 2023)

Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl). - Jules Jacobs; Jonas Kastberg Hinrichsen; Robbert Krebbers (Proc. ACM Program. Lang., 2023)

Unification for Subformula Linking under Quantifiers. - Ike Mulder; Robbert Krebbers (CPP, 2024)

Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. - Marc Hermes; Robbert Krebbers (ITP, 2024)

RefinedRust: A Type System for High-Assurance Verification of Rust Programs. - Lennard Gäher; Michael Sammler; Ralf Jung 002; Robbert Krebbers; Derek Dreyer (Proc. ACM Program. Lang., 2024)

Multris: Functional Verification of Multiparty Message Passing in Separation Logic. - Jonas Kastberg Hinrichsen; Jules Jacobs; Robbert Krebbers (Proc. ACM Program. Lang., 2024)

A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. - Sunho Park; Jaewoo Kim; Ike Mulder; Jaehwang Jung; Janggun Lee; Robbert Krebbers; Jeehoon Kang (Proc. ACM Program. Lang., 2024)

Verified Lock-Free Session Channels with Linking. - Thomas Somers 001; Robbert Krebbers (Proc. ACM Program. Lang., 2024)

Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. - Jules Jacobs; Jonas Kastberg Hinrichsen; Robbert Krebbers (Proc. ACM Program. Lang., 2024)

A Logical Approach to Type Soundness. - Amin Timany; Robbert Krebbers; Derek Dreyer; Lars Birkedal (J. ACM, 2024)

Affect: An Affine Type and Effect System. - Orpheas van Rooij; Robbert Krebbers (Proc. ACM Program. Lang., 2025)