Simon Friis Vindum

According to our database, Simon Friis Vindum authored at least 9 papers between 2020 and 2025.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2025

The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic.

Simon Friis Vindum, Aïna Linn Georges, Lars Birkedal

Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2025

2023

Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory.

Simon Friis Vindum, Lars Birkedal

Proc. ACM Program. Lang., October, 2023

Artifact for the paper "Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory" in OOPSLA23.

Simon Friis Vindum, Lars Birkedal

Dataset, September, 2023

Artifact for the paper "Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory" in OOPSLA23.

Simon Friis Vindum, Lars Birkedal

Dataset, September, 2023

2022

Mechanized verification of a fine-grained concurrent queue from meta's folly library.

Simon Friis Vindum, Dan Frumin, Lars Birkedal

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2021

Coq development for "Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library".

Simon Friis Vindum, Dan Frumin, Lars Birkedal

Dataset, December, 2021

Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library - Coq Artefact.

Simon Friis Vindum, Dan Frumin, Lars Birkedal

Dataset, December, 2021

Contextual refinement of the Michael-Scott queue (proof pearl).

Simon Friis Vindum, Lars Birkedal

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

Contextual Refinement of the Michael-Scott Queue - Coq Artifact.

Simon Friis Vindum, Lars Birkedal

Dataset, December, 2020