default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDRobbert Krebbers
Person information
- affiliation: Radboud University Nijmegen, The Netherlands
SPARQL queries 
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, Jules Jacobs, Robbert Krebbers:
Multris: Functional Verification of Multiparty Message Passing in Separation Logic. Proc. ACM Program. Lang. 8(OOPSLA2): 1446-1474 (2024) - [j29]Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang:
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. Proc. ACM Program. Lang. 8(PLDI): 175-198 (2024) - [j28]Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer:
RefinedRust: A Type System for High-Assurance Verification of Rust Programs. Proc. ACM Program. Lang. 8(PLDI): 1115-1139 (2024) - [j27]Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers:
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, Robbert Krebbers:
Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. ITP 2024: 19:1-19:18 - [e2]Venanzio Capretta, Robbert Krebbers, Freek Wiedijk:
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, Jonas Kastberg Hinrichsen, Robbert Krebbers:
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl). Proc. ACM Program. Lang. 7(ICFP): 768-795 (2023) - [j25]Ike Mulder, Robbert Krebbers:
Proof Automation for Linearizability in Separation Logic. Proc. ACM Program. Lang. 7(OOPSLA1): 462-491 (2023) - [j24]Ike Mulder, Lukasz Czajka, Robbert Krebbers:
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. Proc. ACM Program. Lang. 7(PLDI): 1340-1364 (2023) - [j23]Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer:
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, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer:
Later credits: resourceful reasoning for the later modality. Proc. ACM Program. Lang. 6(ICFP): 283-311 (2022) - [j20]Jules Jacobs, Stephanie Balzer, Robbert Krebbers:
Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang. 6(ICFP): 466-495 (2022) - [j19]Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer:
Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang. 6(POPL): 1-31 (2022) - [j18]Jules Jacobs, Stephanie Balzer, Robbert Krebbers:
Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang. 6(POPL): 1-33 (2022) - [j17]Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell:
VIP: verifying real-world C idioms with integer-pointer casts. Proc. ACM Program. Lang. 6(POPL): 1-32 (2022) - [c22]Ike Mulder, Robbert Krebbers, Herman Geuvers:
Diaframe: automated verification of fine-grained concurrent programs in Iris. PLDI 2022: 809-824 - 2021
- [j16]Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer:
Safe systems programming in Rust. Commun. ACM 64(4): 144-152 (2021) - [j15]Dan Frumin, Robbert Krebbers, Lars Birkedal:
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, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson:
Machine-checked semantic session typing. CPP 2021: 178-198 - [c20]Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal:
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, Lars Birkedal, Robbert Krebbers:
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, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser:
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, Jesper Bengtson, Robbert Krebbers:
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, Robbert Krebbers, Lars Birkedal:
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, Robbert Krebbers, Lars Birkedal:
Iron: managing obligations in higher-order concurrent separation logic. Proc. ACM Program. Lang. 3(POPL): 65:1-65:30 (2019) - [c16]Dan Frumin, Léon Gondelman, Robbert Krebbers:
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, Sjaak Smetsers, Freek Verbeek, Benoît Viguier, Freek Wiedijk:
A benchmark for C program verification. CoRR abs/1904.01009 (2019) - [i4]Dan Frumin, Robbert Krebbers, Lars Birkedal:
Compositional Non-Interference for Fine-Grained Concurrent Programs. CoRR abs/1910.00905 (2019) - 2018
- [j9]Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer:
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, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer:
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, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser:
Intrinsically-typed definitional interpreters for imperative languages. Proc. ACM Program. Lang. 2(POPL): 16:1-16:34 (2018) - [j5]Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer:
RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL): 66:1-66:34 (2018) - [c15]Dan Frumin, Robbert Krebbers, Lars Birkedal:
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. LICS 2018: 442-451 - 2017
- [c14]Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal:
The Essence of Higher-Order Concurrent Separation Logic. ESOP 2017: 696-723 - [c13]Robbert Krebbers, Amin Timany, Lars Birkedal:
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, Robbert Krebbers, Lars Birkedal, Derek Dreyer:
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:
