Commits · 7f62234d622a199a039a87da5ecf37a1e4599485 · Iris / Actris

Dec 16, 2020
- Silent some warnings (as in Iris). · d21f89df
  Robbert Krebbers authored 4 years ago
  
  d21f89df
Dec 02, 2020
- Added equivalence lemmas for iProto_message and iProto_choice · 6dfa5f72
  Jonas Kastberg authored 4 years ago
  
  6dfa5f72
Nov 13, 2020
- Added example of rpc client/service · d7f2e1a0
  Jonas Kastberg authored 4 years ago
  
  d7f2e1a0
Oct 27, 2020
- Renamed map.v -> par_map.v to distinguish from swap_mapper.v · 2528ab76
  Jonas Kastberg authored 4 years ago
  
  2528ab76
Sep 22, 2020
- Rename environment → context + some random cleanup along the way. · 13215e11
  Robbert Krebbers authored 4 years ago
  
  13215e11
- Refactored list type to own file. Bumped mapper_list. Documentation. · 36b0408d
  Jonas Kastberg authored 4 years ago
  
  36b0408d
- Renamed double.v -> par_recv.v · 51b34e7e
  Jonas Kastberg authored 4 years ago
  
  51b34e7e
Sep 21, 2020
- Refactoring of client/service · fdc2775d
  Jonas Kastberg authored 4 years ago
  
  fdc2775d
- Added example of computation service with producer/consumer client · e2940752
  Jonas Kastberg authored 4 years ago
  
  e2940752
Sep 17, 2020
- Added typing example for uncheckable mapper · c1ed805c
  Jonas Kastberg authored 4 years ago
  
  c1ed805c
- Added type former for a type appended N times · 661e6d86
  Jonas Kastberg authored 4 years ago
  
  661e6d86
- Separate file for session typing rules. · a92c3f40
  Robbert Krebbers authored 4 years ago
  
  a92c3f40
Sep 16, 2020

Squashed commit of the following: · 2dc8d5d8

Jonas Kastberg authored 4 years ago

commit e0d15199
Author: jihgfee <jihgfee@gmail.com>
Date:   Wed Sep 16 14:20:00 2020 +0200

    Refactoring - Moved spar to own file and renamed as par_start

commit fd7dc61d
Author: jihgfee <jihgfee@gmail.com>
Date:   Wed Sep 16 13:10:42 2020 +0200

    Proved spar using typing rule instead of breaking abstraction

commit 821a4c23
Author: jihgfee <jihgfee@gmail.com>
Date:   Tue Sep 15 17:11:20 2020 +0200

    Whitespace cleanup

commit eb01938a
Author: jihgfee <jihgfee@gmail.com>
Date:   Tue Sep 15 17:10:37 2020 +0200

    Added a parallel composition for lambdas over channels

2dc8d5d8

Sep 03, 2020
- sync warning settings · 780f5518
  Ralf Jung authored 4 years ago
  
  780f5518
Aug 26, 2020
- Added list reverse example · 4c8002f8
  Jonas Kastberg authored 4 years ago
  
  4c8002f8
Aug 15, 2020
- Added flag to prevent warnings from Coq 8.12 bump · ed16401e
  Jonas Kastberg authored 4 years ago
  
  ed16401e
Aug 07, 2020
- Lifted program reuse to mapper example · 901d37f7
  Jonas Kastberg authored 4 years ago
  
  901d37f7
Jul 24, 2020
- First naive proof of the swap mapper subprotocol relation · 5d08f0e8
  Jonas Kastberg authored 4 years ago
  
  5d08f0e8
Jun 30, 2020
- Added mapper example to _CoqProject · d7497979
  Jonas Kastberg authored 4 years ago
  
  d7497979
- Added rule to swap branch and select and an example · 0a8289d8
  Jonas Kastberg authored 4 years ago
  
  0a8289d8
Jun 29, 2020
- Renamed file to avoid name clashes · e77f2b4a
  Jonas Kastberg authored 4 years ago
  
  e77f2b4a
Jun 05, 2020
- Added subtyping example to _CoqProject · 1479178d
  Jonas Kastberg authored 4 years ago
  
  1479178d
May 10, 2020
- Rename telescope file. · a15377fd
  Robbert Krebbers authored 4 years ago
  
  a15377fd
May 08, 2020
- Fixed wrong section closing and added exampel to _CoqProject · f00cbb9c
  Jonas Kastberg authored 4 years ago
  
  f00cbb9c
May 05, 2020
- update remaining rules, split mutex into lib · 760d90c0
  Daniël Louwrink authored 4 years ago
  
  760d90c0
May 01, 2020
- WIP: Polymorphic rule for receive · 0942c365
  Jonas Kastberg authored 4 years ago
  
  0942c365
Apr 30, 2020
- Rename. · a07c0c2a
  Robbert Krebbers authored 4 years ago
  
  a07c0c2a
Apr 24, 2020
- Refactor. · 0bc616f0
  Robbert Krebbers authored 4 years ago
  
  Kinded subtyping, better file structure, more setoid stuff, reorganize imports.
  0bc616f0
- Added kinded polymorphism · 8b20b70e
  Jonas Kastberg authored 4 years ago
  
  8b20b70e
Apr 23, 2020
- Added pair typing example · b54a4dc9
  Jonas Kastberg authored 4 years ago
  
  b54a4dc9
Apr 21, 2020
- add rules about copying · fb705371
  Daniël Louwrink authored 4 years ago
  
  fb705371
Apr 13, 2020
- Add `switch` in HeapLang (for n-ary branching). · 73c72d27
  Robbert Krebbers authored 4 years ago
  
  73c72d27
Apr 06, 2020
- Reverted definition of LTyCopy to simply be the Persistent property. · 39127db0
  Jonas Kastberg authored 4 years ago
  
  Added LTyCopy typeclasses for products and sums Removed mutable ref to weak ref subtyping as a consequence.
  39127db0
Mar 31, 2020
- Version of the COFE solver for parametrized functors. · eeaa34dc
  Robbert Krebbers authored 4 years ago
  
  eeaa34dc
Mar 25, 2020
- Make everything work; lots of refactoring. · cd70979b
  Robbert Krebbers authored 5 years ago
  
  cd70979b
- `skipN` function. · 72be456a
  Robbert Krebbers authored 5 years ago
  
  72be456a
Nov 21, 2019
- Bump Iris (make use of `excl_auth`). · 1bcc45db
  Robbert Krebbers authored 5 years ago
  
  1bcc45db
Oct 14, 2019
- Bumped move of Atomic to Iris · 708450ba
  Jonas Kastberg authored 5 years ago
  
  708450ba
- Bumped Coq 8.10 · f55d64b5
  Jonas Kastberg authored 5 years ago
  
  f55d64b5
Oct 12, 2019
- Re-instated missing operator. · f0856ce4
  jihgfee authored 5 years ago
  
  Moved Iris specific stuff into a utility file.
  f0856ce4