Commits · d8a7614727ef9189335fd532020c153fbe61d59d · gradual-typing / sgdt

Jun 18, 2018
- completeness for contextual preorder · d8a76147
  Max New authored 6 years ago
  
  d8a76147
- new notation for lr congruence proofs · 4cff3fbb
  Max New authored 6 years ago
  
  4cff3fbb
- update lr definition with new notation · 6f1b7a09
  Max New authored 6 years ago
  
  6f1b7a09
- Merge branch 'master' of github.ccs.neu.edu:coqatoos/cbv-gradual-type-theory · c4cec275
  Max New authored 6 years ago
  
  c4cec275
- dynamic types · 32578d2e
  Max New authored 6 years ago
  
  32578d2e
- one sfo->ewr worth of typesetting · ad6508ee
  Dan Licata authored 6 years ago
  
  ad6508ee
Jun 16, 2018
- some of the last LR lemmas · 83904411
  Max New authored 6 years ago
  
  83904411
Jun 15, 2018
- sketch some of cbv, start uniqueness principles section · ddb55b64
  Max New authored 6 years ago
  
  ddb55b64
Jun 14, 2018
- more lemmas, rest of cbpv inequations · d263d20c
  Max New authored 6 years ago
  
  d263d20c
- lemmas for the logical relation, almost done · 0be18550
  Max New authored 6 years ago
  
  0be18550
Jun 13, 2018
- proof arch for the lr stuff · 29286821
  Max New authored 6 years ago
  
  29286821
- try to make the lr somewhat clear · 1392c0f8
  Max New authored 6 years ago
  
  1392c0f8
Jun 12, 2018
- start talking about step indexing · 9f1e6ed0
  Max New authored 6 years ago
  
  9f1e6ed0
- the dynamic type is Scheme! · 9fb1e45d
  Max New authored 6 years ago
  
  9fb1e45d
Jun 11, 2018
- some headline theorems · cef6c9ca
  Max New authored 6 years ago
  
  cef6c9ca
May 30, 2018
- one more lemma we'll need · ec564a10
  Max New authored 6 years ago
  
  ec564a10
- define most of the lemmas for the GTT -> CBPV translation · 91c85d90
  Max New authored 6 years ago
  
  91c85d90
May 26, 2018
- some prose · fe7751de
  Max New authored 6 years ago
  
  fe7751de
May 25, 2018

define dynamic type interp, state correctness for translation · 2b3ba963

Max New authored 6 years ago

Conclusion: we should break the contract interpretation into 2 steps:
1. Eliminate the casts using an interpretation for the dyn type tags
2. Complex Value/Stack elimination

2b3ba963

May 24, 2018
- reflexivity, stub of wrapping theorems · 8bee6e9e
  Max New authored 6 years ago
  
  8bee6e9e
- fundamental property, generically over the pole · 3c84c803
  Max New authored 6 years ago
  
  3c84c803
- congruence rules for the globular cbpv · d503d981
  Max New authored 6 years ago
  
  d503d981
- logical relation parameterized by a pole, some more outline · 03d623a3
  Max New authored 6 years ago
  
  03d623a3
- extremely long, but very convincing abstract · 3e6e8e34
  Max New authored 6 years ago
  
  3e6e8e34
May 22, 2018
- write logical relation, proof arch for transitivity, completeness · 9788e29d
  Max New authored 6 years ago
  
  9788e29d
May 21, 2018
- start formalizing the lr · 7870274e
  Max New authored 6 years ago
  
  7870274e
May 12, 2018
- [code] optimizing version of cval elimination, needs renaming for correctness · 01c01516
  Max New authored 6 years ago
  
  01c01516
- [code] add impl of elim complex values using delimited continuations · f0a4061b
  Max New authored 6 years ago
  
  f0a4061b
- show wf blame soundness => thunkable/linear · 3878b2c5
  Max New authored 6 years ago
  
  3878b2c5
May 09, 2018
- some notation for lr and get it to compile · 060921e9
  Max New authored 6 years ago
  
  060921e9
- More abstract, start casts section, stub relation to contextual isos · 3c50b995
  Max New authored 6 years ago
  
  3c50b995
May 08, 2018
- start describing stacks, add blame stub to discussion · 624b776b
  Max New authored 6 years ago
  
  624b776b
- [coq] start working on the coq impl, but stop · 08f14526
  Max New authored 6 years ago
  
  08f14526
- reorg notes · b404ff0d
  Max New authored 6 years ago
  
  b404ff0d
- some intro, and discussion · 21df98ba
  Max New authored 6 years ago
  
  21df98ba
May 06, 2018
- [agda] start implementing renaming · 65a0b1c7
  Max New authored 6 years ago
  
  65a0b1c7
May 05, 2018
- [agda] change names, add upcast cells, need to add substitution · 877c0bfc
  Max New authored 6 years ago
  
  877c0bfc
- [agda] finish value transitivity well-formedness lemma · f946cae3
  Max New authored 6 years ago
  
  f946cae3
- [agda] rewrite with some agdaisms, think it will work now · b6caa730
  Max New authored 6 years ago
  
  b6caa730
May 04, 2018
- start GTT · 2ac80113
  Max New authored 6 years ago
  
  2ac80113