Search

• < Previous
• 1
• Next >

---

Type classes for efficient exact real arithmetic in Coq

Robbert Krebbers ; Bas Spitters.

Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. Previously, we&nbsp;[&hellip;]

---

ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity

Dan Frumin ; Robbert Krebbers ; Lars Birkedal.

We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e \precsim e' : \tau$, which states that a program $e$ refines a&nbsp;[&hellip;]

---

Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic

Jonas Kastberg Hinrichsen ; Jesper Bengtson ; Robbert Krebbers.

Message passing is a useful abstraction for implementing concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for&nbsp;[&hellip;]

---