Commits · arrays · cambium / cosmo · GitLab

Mentions légales du service

Snippets Groups Projects

A GitLab upgrade is scheduled for Monday, June 2, 2025. The service will be unavailable for a few minutes in the morning. We'll keep you posted on the progress of the upgrade on the Mattermost channel: https://mattermost.inria.fr/devel/channels/gitlab. We recommend that you do not work on the platform until an announcement indicates that maintenance is complete.

May 20, 2021
- Merge commit '833f8f37 ' into arrays · a3677636
  Glen Mével authored 4 years ago
  
  a3677636
- rename momm to cosmo (backported from branch `master`) · 3a56f1cf
  Glen Mével authored 4 years ago
  
  3a56f1cf
May 19, 2021
- ICFP21 paper: address some todos · 9ddbbcab
  Glen Mével authored 4 years ago
  
  9ddbbcab
May 17, 2021
- add TODO.txt · 5dbd39a4
  Glen Mével authored 4 years ago
  
  5dbd39a4
Apr 23, 2021
- add author’s response to ICFP reviews · 0093ac30
  Glen Mével authored 4 years ago
  
  0093ac30
- add ICFP reviews · 7c3e679e
  Glen Mével authored 4 years ago
  
  7c3e679e
Apr 21, 2021
- paper: fix typos · 33dee06e
  Glen Mével authored 4 years ago
  
  33dee06e
Mar 08, 2021
- we do not need this old version of mathpartir anymore · 695f2f7f
  Glen Mével authored 4 years ago
  
  695f2f7f
- improve spacing · 6766aa25
  Glen Mével authored 4 years ago
  6766aa25
- use mathpar and mention QueueInv explicitly in figure about weak spec · ca2aae20
  Glen Mével authored 4 years ago
  
  ca2aae20
- improve aspect of vertical triples (brackets are now merged with horizontal... · ef8bbe48
  Glen Mével authored 4 years ago
  ef8bbe48
Mar 05, 2021
- 2-column layout for code of queue · 7ef48542
  Glen Mével authored 4 years ago
  
  7ef48542
- tweak the figure about syntax; add tuples to values · 427dcf15
  Glen Mével authored 4 years ago
  
  427dcf15
- proofread up to \sref{sec:lang} · 5ea6d732
  Glen Mével authored 4 years ago
  
  5ea6d732
Mar 03, 2021
- Paper : remove old comments. Coq : add awp_apply and simplify proofs. · 6707a8e2
  Jacques-Henri Jourdan authored 4 years ago
  
  6707a8e2
- Section pipeline, écrite à l'arrache. · 6fd66f09
  Jacques-Henri Jourdan authored 4 years ago
  
  6fd66f09
- start pipeline · 9b32b3a9
  Glen Mével authored 4 years ago
  
  9b32b3a9
- Typos. · 1bee50b7
  POTTIER Francois authored 4 years ago
  
  1bee50b7
- related work. · facf1372
  Jacques-Henri Jourdan authored 4 years ago
  
  facf1372
- Abstract · 7521322a
  Jacques-Henri Jourdan authored 4 years ago
  
  7521322a
- Merge branch 'arrays' of gitlab.inria.fr:gmevel/cosmo into arrays · dc7399c0
  Jacques-Henri Jourdan authored 4 years ago
  
  dc7399c0
- Avancées sur le related work. · ec5838eb
  Jacques-Henri Jourdan authored 4 years ago
  
  ec5838eb
- Some English fixes in Section 4. · 633a377c
  POTTIER Francois authored 4 years ago
  
  633a377c
- Misc · e42d64ce
  Jacques-Henri Jourdan authored 4 years ago
  
  e42d64ce
- logically atomic triples : change notations to \Phi and \Psi, and comment. · 20a42e6d
  Jacques-Henri Jourdan authored 4 years ago
  
  20a42e6d
- Merge branch 'arrays' of gitlab.inria.fr:gmevel/cosmo into arrays · e7206d14
  Jacques-Henri Jourdan authored 4 years ago
  
  e7206d14
- Change the pipeline invariant according to its Coq proof. · fa4cfb92
  Jacques-Henri Jourdan authored 4 years ago
  
  fa4cfb92
- fin de la preuve de try_enqueue · 36492927
  Glen Mével authored 4 years ago
  
  36492927
- suite de la preuve de try_enqueue · 7f003d15
  Glen Mével authored 4 years ago
  
  7f003d15
- reorganize a bit subsections about the proof and about logical atomicity · 81ab24b6
  Glen Mével authored 4 years ago
  
  81ab24b6
- beginning of proof of try_enqueue · dc73e249
  Glen Mével authored 4 years ago
  
  dc73e249
- definition of logically atomic triples · 7346a433
  Glen Mével authored 4 years ago
  
  7346a433
- Finish the proof of the pipeline. · 3393863e
  Jacques-Henri Jourdan authored 4 years ago
  
  3393863e
Mar 02, 2021
- proof: explain tokens · a5134f98
  Glen Mével authored 4 years ago
  
  a5134f98
- débroussaillage du related work. on commence à y voir un peu plus clair · 8222b90f
  Jacques-Henri Jourdan authored 4 years ago
  
  8222b90f
- ++ proof · 293c07f2
  Glen Mével authored 4 years ago
  
  293c07f2
- linearizability? · c071d827
  Glen Mével authored 4 years ago
  
  c071d827
- Get rid of existential quantifier in invariant-opening rule of logically... · 5515b8f0
  Jacques-Henri Jourdan authored 4 years ago
  5515b8f0
- Merge branch 'arrays' of gitlab.inria.fr:gmevel/cosmo into arrays · 970b8a01
  Jacques-Henri Jourdan authored 4 years ago
  
  970b8a01
- Nitpicks in spec. · 8b8a3190
  Jacques-Henri Jourdan authored 4 years ago
  
  8b8a3190