Travelled to:1 × Italy
1 × USA
Collaborated with:L.Birkedal ∅ F.Wiedijk R.J.0002 A.Bizjak J.Jourdan D.Dreyer D.Frumin L.Gondelman Amin Timany Jonas Kastberg Hinrichsen J.Bengtson Daniel Gratzer C.B.Poulsen Arjen Rouvoet A.Tolmach E.Visser
Talks about:separ (5) logic (5) concurr (3) higher (3) order (3) non (3) determin (2) languag (2) reason (2) type (2)
Person: Robbert Krebbers
DBLP: Krebbers:Robbert
Contributed to:
2014
2013
201720192017201820192020Wrote 9 papers:
- POPL-2014-Krebbers #axiom #c #nondeterminism #semantics #sequence
- An operational and axiomatic semantics for non-determinism and sequence points in C (RK), pp. 101–112.
- FoSSaCS-2013-KrebbersW #control flow #logic
- Separation Logic for Non-local Control Flow and Block Scope Variables (RK, FW), pp. 257–272.
- ESOP-2017-Krebbers0BJDB #concurrent #higher-order #logic
- The Essence of Higher-Order Concurrent Separation Logic (RK, RJ0, AB, JHJ, DD, LB), pp. 696–723.
- ESOP-2019-FruminGK #automation #c #nondeterminism #reasoning
- Semi-automated Reasoning About Non-determinism in C Expressions (DF, LG, RK), pp. 60–87.
- POPL-2017-KrebbersTB #concurrent #higher-order #interactive #logic #proving
- Interactive proofs in higher-order concurrent separation logic (RK, AT, LB), pp. 205–217.
- POPL-2018-0002JKD #named #programming language #rust
- RustBelt: securing the foundations of the rust programming language (RJ0, JHJ, RK, DD), p. 34.
- POPL-2018-PoulsenRTKV #imperative
- Intrinsically-typed definitional interpreters for imperative languages (CBP, AR, AT, RK, EV), p. 34.
- POPL-2019-BizjakGKB #concurrent #higher-order #logic #named
- Iron: managing obligations in higher-order concurrent separation logic (AB, DG, RK, LB), p. 30.
- POPL-2020-HinrichsenBK #logic #named #reasoning
- Actris: session-type based reasoning in separation logic (JKH, JB, RK), p. 30.