Commits · 28bcc853ddaa1570a5569e2677ef6572e110af0f · Iris / lambda-rust · GitLab

Snippets Groups Projects

Jan 23, 2017
- Ref is a type. · 28bcc853
  Jacques-Henri Jourdan authored 8 years ago
  
  28bcc853
- Tweaking refcell. · 6b0f47fc
  Jacques-Henri Jourdan authored 8 years ago
  
  6b0f47fc
- RefCell is a type. · b8916e4a
  Jacques-Henri Jourdan authored 8 years ago
  
  b8916e4a
- Idem for derived kinds of borrows. · ec4c6213
  Jacques-Henri Jourdan authored 8 years ago
  
  ec4c6213
- Simplify proofs related to unique borrows by making borrows respectfull of iff. · f81c0f3a
  Jacques-Henri Jourdan authored 8 years ago
  
  f81c0f3a
Jan 22, 2017
- Use pattern matching for defining some types. This make some proof simpler. · 0259f801
  Jacques-Henri Jourdan authored 8 years ago
  
  0259f801
Jan 21, 2017
- Boxes for function types are part of the function type itself and we do not... · 088802e2
  Jacques-Henri Jourdan authored 8 years ago
  088802e2
- Cell : cleanup a bit. Transform the various primitices into functions. · a2b213bf
  Jacques-Henri Jourdan authored 8 years ago
  
  a2b213bf
Jan 19, 2017
- fix typo in unmk_cell · df18abd2
  Ralf Jung authored 8 years ago
  
  df18abd2
Jan 17, 2017
- don't register instance twice · 6d40a9e8
  Ralf Jung authored 8 years ago
  
  6d40a9e8
Jan 16, 2017
- moar parallel function.v · 1fcdf60b
  Ralf Jung authored 8 years ago
  
  1fcdf60b
Jan 13, 2017
- opam-pins: avoid re-downloading already properly pinned packages · c3027327
  Ralf Jung authored 8 years ago
  
  c3027327
- opam-ci: avoid re-downloading already properly pinned packages · 5a475f3a
  Ralf Jung authored 8 years ago
  
  5a475f3a
- rename tests -> examples · bfe08683
  Ralf Jung authored 8 years ago
  
  bfe08683
- change notation for memcpy. notation for sum injection has a \Sigma. · 56139a0d
  Ralf Jung authored 8 years ago
  
  56139a0d
Jan 12, 2017
- Revert "rename soundness -> adequacy" · 427363dc
  Jacques-Henri Jourdan authored 8 years ago
  427363dc
- Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq · 50500359
  Jacques-Henri Jourdan authored 8 years ago
  
  50500359
- Fix typo. · be5f96ef
  Jacques-Henri Jourdan authored 8 years ago
  
  be5f96ef
- Simplify proof of soundness/adequacy. · 05bd12cd
  Jacques-Henri Jourdan authored 8 years ago
  
  05bd12cd
Jan 11, 2017
- solve_inG ftw · bb35dbf5
  Ralf Jung authored 8 years ago
  
  bb35dbf5
- rename soundness -> adequacy · 04386c1c
  Ralf Jung authored 8 years ago
  04386c1c
- I can't make a commit with a new file without forgetting to add it... · a25d9f57
  Jacques-Henri Jourdan authored 8 years ago
  
  a25d9f57
- Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq · 6878adc9
  Jacques-Henri Jourdan authored 8 years ago
  6878adc9
- Soundness of the type system. Also, added a file typing.v that reexports all the type system. · 4e8ad785
  Jacques-Henri Jourdan authored 8 years ago
  
  4e8ad785
- lang/heap: do sealing with primitive projections · d22a2899
  Ralf Jung authored 8 years ago
  
  d22a2899
- Make it possible to nest uninit products for subtyping. · 06fa8d5b
  Jacques-Henri Jourdan authored 8 years ago
  
  06fa8d5b
Jan 10, 2017
- Alpha renaming. · d63de7cb
  Jacques-Henri Jourdan authored 8 years ago
  
  d63de7cb
- Have subtyping between product of uninit and uninit automatically proved. · 4b213366
  Jacques-Henri Jourdan authored 8 years ago
  
  4b213366
- More uses of [iDestruct ty_size_eq]. · 7c432dd7
  Jacques-Henri Jourdan authored 8 years ago
  
  7c432dd7
- Forgot a file. · 0a2c58c0
  Jacques-Henri Jourdan authored 8 years ago
  
  0a2c58c0
- Cleaning : remove hints about [product2] from solve_typing (this type is only... · af680b50
  Jacques-Henri Jourdan authored 8 years ago
  af680b50
- Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq · aab16b4b
  Jacques-Henri Jourdan authored 8 years ago
  
  aab16b4b
- Typechecked lazy lifetime initialization. Also, switched from eauto to... · d028499f
  Jacques-Henri Jourdan authored 8 years ago
  d028499f
- use the fact that we can specialize lemmas below later · a7eff7e2
  Ralf Jung authored 8 years ago
  
  a7eff7e2
- Typechecking unwrap_or. · b643319a
  Jacques-Henri Jourdan authored 8 years ago
  
  b643319a
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq · 19706709
  Ralf Jung authored 8 years ago
  
  19706709
- prove writing to Cell; tune some notation · 62785d61
  Ralf Jung authored 8 years ago
  
  62785d61
- Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq · 4e19edb8
  Jacques-Henri Jourdan authored 8 years ago
  4e19edb8
- Type-checking option_as_mut. · 261c1966
  Jacques-Henri Jourdan authored 8 years ago
  
  261c1966
- forgot to add cell to _CoqProject · 0c861568
  Ralf Jung authored 8 years ago
  
  0c861568