default search action
Robbert Krebbers
Person information
- affiliation: Radboud University Nijmegen, The Netherlands
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j31]Thomas Somers
, Robbert Krebbers
Verified Lock-Free Session Channels with Linking. Proc. ACM Program. Lang. 8(OOPSLA2): 588-617 (2024) - [j30]Jonas Kastberg Hinrichsen
Multris: Functional Verification of Multiparty Message Passing in Separation Logic. Proc. ACM Program. Lang. 8(OOPSLA2): 1446-1474 (2024) - [j29]Sunho Park
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. Proc. ACM Program. Lang. 8(PLDI): 175-198 (2024) - [j28]Lennard Gäher
RefinedRust: A Type System for High-Assurance Verification of Rust Programs. Proc. ACM Program. Lang. 8(PLDI): 1115-1139 (2024) - [j27]Jules Jacobs
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. Proc. ACM Program. Lang. 8(POPL): 1385-1417 (2024) - [c25]Ike Mulder, Robbert Krebbers:
Unification for Subformula Linking under Quantifiers. CPP 2024: 75-88 - [c24]Marc Hermes
Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. ITP 2024: 19:1-19:18 - [e2]Venanzio Capretta
Logics and Type Systems in Theory and Practice - Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday. Lecture Notes in Computer Science 14560, Springer 2024, ISBN 978-3-031-61715-7 [contents] - 2023
- [j26]Jules Jacobs
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl). Proc. ACM Program. Lang. 7(ICFP): 768-795 (2023) - [j25]Ike Mulder
Proof Automation for Linearizability in Separation Logic. Proc. ACM Program. Lang. 7(OOPSLA1): 462-491 (2023) - [j24]Ike Mulder
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. Proc. ACM Program. Lang. 7(PLDI): 1340-1364 (2023) - [j23]Michael Sammler
DimSum: A Decentralized Approach to Multi-language Semantics and Verification. Proc. ACM Program. Lang. 7(POPL): 775-805 (2023) - [c23]Robbert Krebbers:
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). ITP 2023: 2:1-2:1 - [e1]Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic:
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. ACM 2023 [contents] - 2022
- [j22]Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers:
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. Log. Methods Comput. Sci. 18(2) (2022) - [j21]Simon Spies
Later credits: resourceful reasoning for the later modality. Proc. ACM Program. Lang. 6(ICFP): 283-311 (2022) - [j20]Jules Jacobs
Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang. 6(ICFP): 466-495 (2022) - [j19]Lennard Gäher
Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang. 6(POPL): 1-31 (2022) - [j18]Jules Jacobs
Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang. 6(POPL): 1-33 (2022) - [j17]Rodolphe Lepigre
VIP: verifying real-world C idioms with integer-pointer casts. Proc. ACM Program. Lang. 6(POPL): 1-32 (2022) - [c22]Ike Mulder
Diaframe: automated verification of fine-grained concurrent programs in Iris. PLDI 2022: 809-824 - 2021
- [j16]Ralf Jung
Safe systems programming in Rust. Commun. ACM 64(4): 144-152 (2021) - [j15]Dan Frumin
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. Log. Methods Comput. Sci. 17(3) (2021) - [j14]Arjen Rouvoet, Robbert Krebbers, Eelco Visser:
Intrinsically typed compilation with nameless labels. Proc. ACM Program. Lang. 5(POPL): 1-28 (2021) - [c21]Jonas Kastberg Hinrichsen
Machine-checked semantic session typing. CPP 2021: 178-198 - [c20]Simon Spies, Lennard Gäher, Daniel Gratzer
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. PLDI 2021: 80-95 - [c19]Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
RefinedC: automating the foundational verification of C code with refined ownership types. PLDI 2021: 158-174 - [c18]Dan Frumin, Robbert Krebbers, Lars Birkedal:
Compositional Non-Interference for Fine-Grained Concurrent Programs. SP 2021: 1416-1433 - 2020
- [j13]Paolo G. Giarrusso, Léo Stefanesco, Amin Timany
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. Proc. ACM Program. Lang. 4(ICFP): 114:1-114:29 (2020) - [j12]Arjen Rouvoet, Hendrik van Antwerpen
Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications. Proc. ACM Program. Lang. 4(OOPSLA): 180:1-180:28 (2020) - [j11]Jonas Kastberg Hinrichsen
Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang. 4(POPL): 6:1-6:30 (2020) - [c17]Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser:
Intrinsically-typed definitional interpreters for linear, session-typed languages. CPP 2020: 284-298 - [i7]Dan Frumin
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. CoRR abs/2006.13635 (2020) - [i6]Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers:
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. CoRR abs/2010.15030 (2020)
2010 – 2019
- 2019
- [j10]Ales Bizjak, Daniel Gratzer
Iron: managing obligations in higher-order concurrent separation logic. Proc. ACM Program. Lang. 3(POPL): 65:1-65:30 (2019) - [c16]Dan Frumin
Semi-automated Reasoning About Non-determinism in C Expressions. ESOP 2019: 60-87 - [i5]Marko C. J. D. van Eekelen, Daniil Frumin, Herman Geuvers, Léon Gondelman, Robbert Krebbers, Marc Schoolderman
A benchmark for C program verification. CoRR abs/1904.01009 (2019) - [i4]Dan Frumin
Compositional Non-Interference for Fine-Grained Concurrent Programs. CoRR abs/1910.00905 (2019) - 2018
- [j9]Ralf Jung
Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28: e20 (2018) - [j8]Robbert Krebbers, Jacques-Henri Jourdan
MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. 2(ICFP): 77:1-77:30 (2018) - [j7]Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer:
Mtac2: typed tactics for backward reasoning in Coq. Proc. ACM Program. Lang. 2(ICFP): 78:1-78:31 (2018) - [j6]Casper Bach Poulsen
Intrinsically-typed definitional interpreters for imperative languages. Proc. ACM Program. Lang. 2(POPL): 16:1-16:34 (2018) - [j5]Ralf Jung
RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL): 66:1-66:34 (2018) - [c15]Dan Frumin
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. LICS 2018: 442-451 - 2017
- [c14]Robbert Krebbers, Ralf Jung
The Essence of Higher-Order Concurrent Separation Logic. ESOP 2017: 696-723 - [c13]Robbert Krebbers, Amin Timany
Interactive proofs in higher-order concurrent separation logic. POPL 2017: 205-217 - 2016
- [j4]Robbert Krebbers:
A Formal C Memory Model for Separation Logic. J. Autom. Reason. 57(4): 319-387 (2016) - [c12]Robbert Krebbers, Louis Parlant, Alexandra Silva:
Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq. Theory and Practice of Formal Methods 2016: 309-324 - [c11]Ralf Jung
Higher-order ghost state. ICFP 2016: 256-269 - 2015
- [c10]Robbert Krebbers, Freek Wiedijk:
A Typed C11 Semantics for Interactive Theorem Proving. CPP 2015: 15-27 - [i3]Robbert Krebbers:
A Formal C Memory Model for Separation Logic. CoRR abs/1509.03339 (2015) - 2014
- [c9]Robbert Krebbers, Xavier Leroy, Freek Wiedijk:
Formal C Semantics: CompCert and the C Standard. ITP 2014: 543-548 - [c8]Robbert Krebbers:
An operational and axiomatic semantics for non-determinism and sequence points in C. POPL 2014: 101-112 - [c7]Robbert Krebbers:
Separation Algebras for C Verification in Coq. VSTTE 2014: 150-166 - 2013
- [j3]Herman Geuvers, Robbert Krebbers, James McKinna:
The λμT-calculus. Ann. Pure Appl. Log. 164(6): 676-701 (2013) - [c6]Robbert Krebbers:
Aliasing Restrictions of C11 Formalized in Coq. CPP 2013: 50-65 - [c5]Robbert Krebbers, Freek Wiedijk:
Separation Logic for Non-local Control Flow and Block Scope Variables. FoSSaCS 2013: 257-272 - 2012
- [c4]Robbert Krebbers:
A call-by-value lambda-calculus with lists and control. CL&C 2012: 19-33 - [i2]Herman Geuvers, Robbert Krebbers, James McKinna:
The lambda-mu-T-calculus. CoRR abs/1204.0347 (2012) - 2011
- [j2]Robbert Krebbers, Bas Spitters
Type classes for efficient exact real arithmetic in Coq. Log. Methods Comput. Sci. 9(1) (2011) - [j1]Herman Geuvers, Robbert Krebbers:
The correctness of Newman's typability algorithm and some of its extensions. Theor. Comput. Sci. 412(28): 3242-3261 (2011) - [c3]Robbert Krebbers, Bas Spitters
Computer Certified Efficient Exact Reals in Coq. Calculemus/MKM 2011: 90-106 - [c2]Robbert Krebbers, Freek Wiedijk:
A Formalization of the C99 Standard in HOL, Isabelle and Coq. Calculemus/MKM 2011: 301-303 - [i1]Robbert Krebbers, Bas Spitters:
Computer certified efficient exact reals in Coq. CoRR abs/1105.2751 (2011) - 2010
- [c1]Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk:
Pure Type Systems without Explicit Contexts. LFMTP 2010: 53-67
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-02 21:27 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: