Logical Relations
Todo:
- n-ary branching
- Add copy subtyping
- Polymorphism in protocols
- Channel Mutexes
Edited by Jonas Kastberg
Merge request reports
Activity
added 2 commits
added 38 commits
-
e3156444...32a6cf2d - 2 commits from branch
master
- 1867e151 - Added the logical relations by Daniel Louwrink.
- 4efc45b6 - Added Initial subtyping relation and trivial rules
- b7003b98 - Added notation for subtyping relation(s)
- 527e1c1a - Tweak subtyping and misc code clean up.
- 4f6277dc - Added Subsumption Theorem
- 6f580a14 - Bumped Iris
- 0cf2f0cb - Proven transitivity of subtyping and last recursive subtyping
- 14f2a8b5 - Added subtyping of mutexes
- 2a44ab67 - Renamed ref and weakref to ref_mut and ref_shr respectively
- a457727f - Added copy typeclasses for constants and unified share and mutable ref programs
- 8e8115b6 - nits
- c62f8aec - Added subtyping for protocols
- 1b8f03c1 - Added subtyping of dual protocols
- 99f87bf7 - Nits, and added 2 out of 3 recursive protocol subtypings
- 173c2106 - Added bool copy typeclass
- 4d09dc5b - Added operator typing
- 2e0b02d2 - Bumped master
- 58439041 - WIP swap subtyping rule
- 7d97d1d2 - Finalized swap rule proof
- bf394d05 - Reverted definition of LTyCopy to simply be the Persistent property.
- 8e64f375 - Added later in premises of subtyping rules
- 455b5f14 - Nits
- a256ec45 - Added more copy typeclasses and nits
- c660d647 - More laters in premises of subtype rules
- ce0a9680 - Added recursive subtyping on protocols
- 29c6a2b0 - Added anti-symmetry relation for subtyping
- 4c21e34f - Added quantification over protocols in base types
- 5cb42172 - Added append subtyping
- 8eb0ba59 - Added laters to universal quantifier
- 19486c40 - Refactored chan_rules into two files - type definition and instances
- e41ef172 - nits
- 7229fa80 - Clean Up
- 5cbc40c6 - Laters in premises of arrow subtyping
- c3c0fdfb - nits
- b8e94cd9 - Actually removed refactored definition of lproto
- db9b78f0 - Bumped is_lock Contractive instance
Toggle commit list-
e3156444...32a6cf2d - 2 commits from branch
marked as a Work In Progress from 58439041
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
Please register or sign in to reply