publications: - title: "Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Louis Parlant" link: "https://researchr.org/alias/louis-parlant" - name: "Alexandra Silva" link: "https://researchr.org/alias/alexandra-silva" year: "2016" doi: "http://dx.doi.org/10.1007/978-3-319-30734-3_21" links: doi: "http://dx.doi.org/10.1007/978-3-319-30734-3_21" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/birthday/KrebbersPS16" researchr: "https://researchr.org/publication/KrebbersPS16" cites: 0 citedby: 0 pages: "309-324" booktitle: "BIRTHDAY" kind: "inproceedings" key: "KrebbersPS16" - title: "Higher-order ghost state" author: - name: "Ralf Jung 0002" link: "https://researchr.org/alias/ralf-jung-0002" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" - name: "Derek Dreyer" link: "https://researchr.org/alias/derek-dreyer" year: "2016" doi: "http://doi.acm.org/10.1145/2951913.2951943" links: doi: "http://doi.acm.org/10.1145/2951913.2951943" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/icfp/0002KBD16" researchr: "https://researchr.org/publication/0002KBD16" cites: 0 citedby: 0 pages: "256-269" booktitle: "ICFP" kind: "inproceedings" key: "0002KBD16" - title: "Separation Algebras for C Verification in Coq" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" year: "2014" doi: "http://dx.doi.org/10.1007/978-3-319-12154-3_10" links: doi: "http://dx.doi.org/10.1007/978-3-319-12154-3_10" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/vstte/Krebbers14" researchr: "https://researchr.org/publication/Krebbers14-0" cites: 0 citedby: 0 pages: "150-166" booktitle: "vstte" kind: "inproceedings" key: "Krebbers14-0" - title: "T-calculus" author: - name: "Herman Geuvers" link: "https://researchr.org/alias/herman-geuvers" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "James McKinna" link: "https://researchr.org/alias/james-mckinna" year: "2013" doi: "http://dx.doi.org/10.1016/j.apal.2012.05.005" links: doi: "http://dx.doi.org/10.1016/j.apal.2012.05.005" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/apal/GeuversKM13" researchr: "https://researchr.org/publication/GeuversKM13" cites: 0 citedby: 0 journal: "APAL" volume: "164" number: "6" pages: "676-701" kind: "article" key: "GeuversKM13" - title: "The correctness of Newman s typability algorithm and some of its extensions" author: - name: "Herman Geuvers" link: "https://researchr.org/alias/herman-geuvers" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" year: "2011" doi: "http://dx.doi.org/10.1016/j.tcs.2011.03.016" links: doi: "http://dx.doi.org/10.1016/j.tcs.2011.03.016" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/tcs/GeuversK11" researchr: "https://researchr.org/publication/GeuversK11" cites: 0 citedby: 0 journal: "TCS" volume: "412" number: "28" pages: "3242-3261" kind: "article" key: "GeuversK11" - title: "Iron: managing obligations in higher-order concurrent separation logic" author: - name: "Ales Bizjak" link: "https://researchr.org/alias/ales-bizjak" - name: "Daniel Gratzer" link: "https://researchr.org/alias/daniel-gratzer" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" year: "2019" doi: "https://dl.acm.org/citation.cfm?id=3290378" links: doi: "https://dl.acm.org/citation.cfm?id=3290378" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/BizjakGKB19" researchr: "https://researchr.org/publication/BizjakGKB19" cites: 0 citedby: 0 journal: "PACMPL" volume: "3" kind: "article" key: "BizjakGKB19" - title: "RustBelt: securing the foundations of the rust programming language" author: - name: "Ralf Jung" link: "https://researchr.org/alias/ralf-jung" - name: "Jacques-Henri Jourdan" link: "https://researchr.org/alias/jacques-henri-jourdan" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Derek Dreyer" link: "https://researchr.org/alias/derek-dreyer" year: "2018" doi: "http://doi.acm.org/10.1145/3158154" links: doi: "http://doi.acm.org/10.1145/3158154" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/0002JKD18" researchr: "https://researchr.org/publication/JungJKD18" cites: 0 citedby: 0 journal: "PACMPL" volume: "2" number: "POPL" kind: "article" key: "JungJKD18" - title: "Interactive proofs in higher-order concurrent separation logic" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Amin Timany" link: "https://researchr.org/alias/amin-timany" - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" year: "2017" doi: "http://dl.acm.org/citation.cfm?id=3009855" links: doi: "http://dl.acm.org/citation.cfm?id=3009855" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/KrebbersTB17" researchr: "https://researchr.org/publication/KrebbersTB17" cites: 0 citedby: 0 pages: "205-217" booktitle: "POPL" kind: "inproceedings" key: "KrebbersTB17" - title: "MoSeL: a general, extensible modal framework for interactive proofs in separation logic" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Jacques-Henri Jourdan" link: "https://researchr.org/alias/jacques-henri-jourdan" - name: "Ralf Jung 0002" link: "https://researchr.org/alias/ralf-jung-0002" - name: "Joseph Tassarotti" link: "https://researchr.org/alias/joseph-tassarotti" - name: "Jan-Oliver Kaiser" link: "https://researchr.org/alias/jan-oliver-kaiser" - name: "Amin Timany" link: "https://researchr.org/alias/amin-timany" - name: "Arthur Charguéraud" link: "https://researchr.org/alias/arthur-chargu%C3%A9raud" - name: "Derek Dreyer" link: "https://researchr.org/alias/derek-dreyer" year: "2018" doi: "https://doi.org/10.1145/3236772" links: doi: "https://doi.org/10.1145/3236772" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/KrebbersJ0TKTCD18" researchr: "https://researchr.org/publication/KrebbersJ0TKTCD18" cites: 0 citedby: 0 journal: "PACMPL" volume: "2" number: "ICFP" kind: "article" key: "KrebbersJ0TKTCD18" - title: "An operational and axiomatic semantics for non-determinism and sequence points in C" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" year: "2014" doi: "http://doi.acm.org/10.1145/2535838.2535878" links: doi: "http://doi.acm.org/10.1145/2535838.2535878" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/popl/Krebbers14" researchr: "https://researchr.org/publication/Krebbers14" cites: 0 citedby: 0 pages: "101-112" booktitle: "POPL" kind: "inproceedings" key: "Krebbers14" - title: "The Essence of Higher-Order Concurrent Separation Logic" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Ralf Jung 0002" link: "https://researchr.org/alias/ralf-jung-0002" - name: "Ales Bizjak" link: "https://researchr.org/alias/ales-bizjak" - name: "Jacques-Henri Jourdan" link: "https://researchr.org/alias/jacques-henri-jourdan" - name: "Derek Dreyer" link: "https://researchr.org/alias/derek-dreyer" - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" year: "2017" doi: "http://dx.doi.org/10.1007/978-3-662-54434-1_26" links: doi: "http://dx.doi.org/10.1007/978-3-662-54434-1_26" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/Krebbers0BJDB17" researchr: "https://researchr.org/publication/Krebbers0BJDB17" cites: 0 citedby: 0 pages: "696-723" booktitle: "ESOP" kind: "inproceedings" key: "Krebbers0BJDB17" - title: "Intrinsically-typed definitional interpreters for linear, session-typed languages" author: - name: "Arjen Rouvoet" link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2020" doi: "https://doi.org/10.1145/3372885.3373818" abstract: "An intrinsically-typed definitional interpreter is a concise specification of dynamic semantics, that is executable and type safe by construction. Unfortunately, scaling intrinsically-typed definitional interpreters to more complicated object languages often results in definitions that are cluttered with manual proof work. For linearly-typed languages (including session-typed languages) one has to prove that the interpreter, as well as all the operations on semantic components, treat values linearly. We present new methods and tools that make it possible to implement intrinsically-typed definitional interpreters for linearly-typed languages in a way that hides the majority of the manual proof work. Inspired by separation logic, we develop reusable and composable abstractions for programming with linear operations using dependent types. Using these abstractions, we define interpreters for linear lambda calculi with strong references, concurrency, and session-typed communication in Agda." links: doi: "https://doi.org/10.1145/3372885.3373818" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/RouvoetPKV20" researchr: "https://researchr.org/publication/RouvoetPKV20" cites: 0 citedby: 0 pages: "284-298" booktitle: "CPP" kind: "inproceedings" key: "RouvoetPKV20" - title: "A Formal C Memory Model for Separation Logic" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" year: "2016" doi: "http://dx.doi.org/10.1007/s10817-016-9369-1" links: doi: "http://dx.doi.org/10.1007/s10817-016-9369-1" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jar/Krebbers16" researchr: "https://researchr.org/publication/Krebbers16" cites: 0 citedby: 0 journal: "JAR" volume: "57" number: "4" pages: "319-387" kind: "article" key: "Krebbers16" - title: "Actris: session-type based reasoning in separation logic" author: - name: "Jonas Kastberg Hinrichsen" link: "https://researchr.org/alias/jonas-kastberg-hinrichsen" - name: "Jesper Bengtson" link: "https://researchr.org/alias/jesper-bengtson" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" year: "2020" doi: "https://doi.org/10.1145/3371074" links: doi: "https://doi.org/10.1145/3371074" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/HinrichsenBK20" researchr: "https://researchr.org/publication/HinrichsenBK20" cites: 0 citedby: 0 journal: "PACMPL" volume: "4" number: "POPL" kind: "article" key: "HinrichsenBK20" - title: "A Formalization of the C99 Standard in HOL, Isabelle and Coq" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Freek Wiedijk" link: "https://researchr.org/alias/freek-wiedijk" year: "2011" doi: "http://dx.doi.org/10.1007/978-3-642-22673-1_28" links: doi: "http://dx.doi.org/10.1007/978-3-642-22673-1_28" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/mkm/KrebbersW11" researchr: "https://researchr.org/publication/KrebbersW11" cites: 0 citedby: 0 pages: "301-303" booktitle: "mkm" kind: "inproceedings" key: "KrebbersW11" - title: "Intrinsically-typed definitional interpreters for imperative languages" author: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Arjen Rouvoet" link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2018" doi: "http://doi.acm.org/10.1145/3158104" abstract: " A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a separate type system requires a separate type safety proof. An alternative approach, at least for pure object languages, is to use a dependently-typed language to encode the object language type system in the definition of the abstract syntax. Using such intrinsically-typed abstract syntax definitions allows the host language type checker to verify automatically that the interpreter satisfies type safety. Does this approach scale to larger and more realistic object languages, and in particular to languages with mutable state and objects? In this paper, we describe and demonstrate techniques and libraries in Agda that successfully scale up intrinsically-typed definitional interpreters to handle rich object languages with non-trivial binding structures and mutable state. While the resulting interpreters are certainly more complex than the simply-typed λ-calculus interpreter we start with, we claim that they still meet the goals of being concise, comprehensible, and executable, while guaranteeing type safety for more elaborate object languages. We make the following contributions: (1) A dependent-passing style technique for hiding the weakening of indexed values as they propagate through monadic code. (2) An Agda library for programming with scope graphs and frames, which provides a uniform approach to dealing with name binding in intrinsically-typed interpreters. (3) Case studies of intrinsically-typed definitional interpreters for the simply-typed λ-calculus with references (STLC+Ref) and for a large subset of Middleweight Java (MJ). " links: doi: "http://doi.acm.org/10.1145/3158104" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/PoulsenRTKV18" technicalreport: "https://researchr.org/publication/preprint-PoulsenRTKV18" tags: - "Intrinsic-Verification" researchr: "https://researchr.org/publication/PoulsenRTKV18" cites: 0 citedby: 0 journal: "PACMPL" volume: "2" number: "POPL" kind: "article" key: "PoulsenRTKV18" - title: "Intrinsically-typed definitional interpreters for imperative languages" author: - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Arjen Rouvoet" link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/" - name: "Andrew P. Tolmach" link: "http://www.cs.pdx.edu/~apt" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2018" abstract: " A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a separate type system requires a separate type safety proof. An alternative approach, at least for pure object languages, is to use a dependently-typed language to encode the object language type system in the definition of the abstract syntax. Using such intrinsically-typed abstract syntax definitions allows the host language type checker to verify automatically that the interpreter satisfies type safety. Does this approach scale to larger and more realistic object languages, and in particular to languages with mutable state and objects? In this paper, we describe and demonstrate techniques and libraries in Agda that successfully scale up intrinsically-typed definitional interpreters to handle rich object languages with non-trivial binding structures and mutable state. While the resulting interpreters are certainly more complex than the simply-typed λ-calculus interpreter we start with, we claim that they still meet the goals of being concise, comprehensible, and executable, while guaranteeing type safety for more elaborate object languages. We make the following contributions: (1) A dependent-passing style technique for hiding the weakening of indexed values as they propagate through monadic code. (2) An Agda library for programming with scope graphs and frames, which provides a uniform approach to dealing with name binding in intrinsically-typed interpreters. (3) Case studies of intrinsically-typed definitional interpreters for the simply-typed λ-calculus with references (STLC+Ref) and for a large subset of Middleweight Java (MJ). " links: published: "https://researchr.org/publication/PoulsenRTKV18" researchr: "https://researchr.org/publication/preprint-PoulsenRTKV18" cites: 0 citedby: 0 type: "Preprint" kind: "techreport" key: "preprint-PoulsenRTKV18" - title: "Separation Logic for Non-local Control Flow and Block Scope Variables" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Freek Wiedijk" link: "https://researchr.org/alias/freek-wiedijk" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-642-37075-5_17" links: doi: "http://dx.doi.org/10.1007/978-3-642-37075-5_17" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/fossacs/KrebbersW13" researchr: "https://researchr.org/publication/KrebbersW13" cites: 0 citedby: 0 pages: "257-272" booktitle: "fossacs" kind: "inproceedings" key: "KrebbersW13" - title: "Formal C Semantics: CompCert and the C Standard" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Xavier Leroy" link: "http://pauillac.inria.fr/~xleroy/" - name: "Freek Wiedijk" link: "https://researchr.org/alias/freek-wiedijk" year: "2014" doi: "http://dx.doi.org/10.1007/978-3-319-08970-6_36" links: doi: "http://dx.doi.org/10.1007/978-3-319-08970-6_36" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/itp/KrebbersLW14" researchr: "https://researchr.org/publication/KrebbersLW14" cites: 0 citedby: 0 pages: "543-548" booktitle: "itp" kind: "inproceedings" key: "KrebbersLW14" - title: "Aliasing Restrictions of C11 Formalized in Coq" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" year: "2013" doi: "http://dx.doi.org/10.1007/978-3-319-03545-1_4" links: doi: "http://dx.doi.org/10.1007/978-3-319-03545-1_4" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/Krebbers13" researchr: "https://researchr.org/publication/Krebbers13" cites: 0 citedby: 0 pages: "50-65" booktitle: "CPP" kind: "inproceedings" key: "Krebbers13" - title: "Mtac2: typed tactics for backward reasoning in Coq" author: - name: "Jan-Oliver Kaiser" link: "https://researchr.org/alias/jan-oliver-kaiser" - name: "Beta Ziliani" link: "https://researchr.org/alias/beta-ziliani" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Yann Régis-Gianas" link: "https://researchr.org/alias/yann-r%C3%A9gis-gianas" - name: "Derek Dreyer" link: "https://researchr.org/alias/derek-dreyer" year: "2018" doi: "https://doi.org/10.1145/3236773" links: doi: "https://doi.org/10.1145/3236773" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/pacmpl/KaiserZKRD18" researchr: "https://researchr.org/publication/KaiserZKRD18" cites: 0 citedby: 0 journal: "PACMPL" volume: "2" number: "ICFP" kind: "article" key: "KaiserZKRD18" - title: "Computer Certified Efficient Exact Reals in Coq" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Bas Spitters" link: "https://researchr.org/alias/bas-spitters" year: "2011" doi: "http://dx.doi.org/10.1007/978-3-642-22673-1_7" links: doi: "http://dx.doi.org/10.1007/978-3-642-22673-1_7" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/mkm/KrebbersS11" researchr: "https://researchr.org/publication/KrebbersS11" cites: 0 citedby: 0 pages: "90-106" booktitle: "mkm" kind: "inproceedings" key: "KrebbersS11" - title: "Iris from the ground up: A modular foundation for higher-order concurrent separation logic" author: - name: "Ralf Jung 0002" link: "https://researchr.org/alias/ralf-jung-0002" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Jacques-Henri Jourdan" link: "https://researchr.org/alias/jacques-henri-jourdan" - name: "Ales Bizjak" link: "https://researchr.org/alias/ales-bizjak" - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" - name: "Derek Dreyer" link: "https://researchr.org/alias/derek-dreyer" year: "2018" doi: "https://doi.org/10.1017/S0956796818000151" links: doi: "https://doi.org/10.1017/S0956796818000151" dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/jfp/JungKJBBD18" researchr: "https://researchr.org/publication/JungKJBBD18" cites: 0 citedby: 0 journal: "JFP" volume: "28" kind: "article" key: "JungKJBBD18" - title: "Knowing When to Ask: Sound scheduling of name resolution in type checkers derived from declarative specifications (Extended Version)" author: - name: "Arjen Rouvoet" link: "https://www.linkedin.com/in/arjen-rouvoet-760347a5/" - name: "Hendrik van Antwerpen" link: "https://nl.linkedin.com/in/hendrikvanantwerpen" - name: "Casper Bach Poulsen" link: "http://www.casperbp.net" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Eelco Visser" link: "http://eelcovisser.org" year: "2020" month: "Oct" doi: "http://doi.org/10.5281/zenodo.4091445" abstract: "There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to automatically obtain type checkers from declarative programming language specifications. This moves the burden of proving correctness from a case-by-case basis for concrete languages to a single correctness proof for the specification language. This vision is obstructed by an aspect common to all programming languages: name resolution. Naming and scoping are pervasive and complex aspects of the static semantics of programming languages. Implementations of type checkers for languages with name binding features such as modules, imports, classes, and inheritance interleave collection of binding information (i.e., declarations, scoping structure, and imports) and querying that information. This requires scheduling those two aspects in such a way that query answers are stable---i.e., they are computed only after all relevant binding structure has been collected. Type checkers for concrete languages accomplish stability using language-specific knowledge about the type system. In this paper we give a language-independent characterization of necessary and sufficient conditions to guarantee stability of name and type queries during type checking in terms of critical edges in an incomplete scope graph. We use critical edges to give a formal small-step operational semantics to a declarative specification language for type systems, that achieves soundness by delaying queries that may depend on missing information. This yields type checkers for the specified languages that are sound by construction---i.e., they schedule queries so that the answers are stable, and only accept programs that are name- and type-correct according to the declarative language specification. We implement this approach, and evaluate it against specifications of a small module and record language, as well as subsets of Java and Scala." links: doi: "http://doi.org/10.5281/zenodo.4091445" successor: "https://researchr.org/publication/RouvoetAPKV20" researchr: "https://researchr.org/publication/RouvoetAPKV20-ext" cites: 0 citedby: 0 publisher: "Zenodo" kind: "inbook" key: "RouvoetAPKV20-ext" - title: "ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency" author: - name: "Dan Frumin" link: "https://researchr.org/alias/dan-frumin" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Lars Birkedal" link: "https://researchr.org/alias/lars-birkedal" year: "2018" doi: "http://doi.acm.org/10.1145/3209108.3209174" links: doi: "http://doi.acm.org/10.1145/3209108.3209174" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/lics/FruminKB18" researchr: "https://researchr.org/publication/FruminKB18" cites: 0 citedby: 0 pages: "442-451" booktitle: "lics" kind: "inproceedings" key: "FruminKB18" - title: "A Typed C11 Semantics for Interactive Theorem Proving" author: - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" - name: "Freek Wiedijk" link: "https://researchr.org/alias/freek-wiedijk" year: "2015" doi: "http://doi.acm.org/10.1145/2676724.2693571" links: doi: "http://doi.acm.org/10.1145/2676724.2693571" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/cpp/KrebbersW15" researchr: "https://researchr.org/publication/KrebbersW15" cites: 0 citedby: 0 pages: "15-27" booktitle: "CPP" kind: "inproceedings" key: "KrebbersW15" - title: "Semi-automated Reasoning About Non-determinism in C Expressions" author: - name: "Dan Frumin" link: "https://researchr.org/alias/dan-frumin" - name: "Léon Gondelman" link: "https://researchr.org/alias/l%C3%A9on-gondelman" - name: "Robbert Krebbers" link: "https://robbertkrebbers.nl" year: "2019" doi: "https://doi.org/10.1007/978-3-030-17184-1_3" links: doi: "https://doi.org/10.1007/978-3-030-17184-1_3" dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/esop/FruminGK19" researchr: "https://researchr.org/publication/FruminGK19" cites: 0 citedby: 0 pages: "60-87" booktitle: "ESOP" kind: "inproceedings" key: "FruminGK19"