Commits · 7768bdf294d5e62b26cf68757739272944d17b95 · gradual-typing / sgdt

Jun 21, 2018
- rest of axiomatic graduality cases · 7768bdf2
  Max New authored 6 years ago
  
  7768bdf2
- Merge branch 'master' of https://github.ccs.neu.edu/coqatoos/cbv-gradual-type-theory · f7a29e66
  Dan Licata authored 6 years ago
  
  f7a29e66
- add cast induction notes for later · 0bc8cd93
  Dan Licata authored 6 years ago
  
  0bc8cd93
Jun 20, 2018
- axiomatic graduality value type compatibility rules · 72f0d382
  Max New authored 6 years ago
  
  72f0d382
- axiomatic graduality computation type compatibility rules · a664c4d5
  Max New authored 6 years ago
  
  a664c4d5
- all ep pair cases except 1 and the base case · 9f655c0c
  Max New authored 6 years ago
  
  9f655c0c
- Merge branch 'master' of https://github.ccs.neu.edu/coqatoos/cbv-gradual-type-theory · c99b7034
  Dan Licata authored 6 years ago
  
  c99b7034
- ep pairs compose, product ep pair proof · 17f8fe12
  Max New authored 6 years ago
  
  17f8fe12
- cast reduction principles, comm conversions, + ep pair case · c5db8fd6
  Max New authored 6 years ago
  
  c5db8fd6
Jun 19, 2018
- start proving contract impls are ep pairs · 96a596b0
  Max New authored 6 years ago
  
  96a596b0
- value, computation ep pair definitions, sketch the coherence proof · 25d841be
  Max New authored 6 years ago
  
  25d841be
- reorder operational semantics and inequational theory sections · d336c923
  Max New authored 6 years ago
  
  d336c923
- fix some notation in LR section · c18e14e8
  Max New authored 6 years ago
  
  c18e14e8
- all eta proofs and beta proofs for recursion · 7e673a4f
  Max New authored 6 years ago
  
  7e673a4f
- Merge branch 'master' of https://github.ccs.neu.edu/coqatoos/cbv-gradual-type-theory · bda938e7
  Dan Licata authored 6 years ago
  
  bda938e7
- edits to GTT figures · 59a89775
  Dan Licata authored 6 years ago
  
  59a89775
Jun 18, 2018
- start writing beta, eta proofs · 8f8c7c88
  Max New authored 6 years ago
  
  8f8c7c88
- delete old pole stuff · 705afef0
  Max New authored 6 years ago
  
  705afef0
- transitivity proof · 067d04f6
  Max New authored 6 years ago
  
  067d04f6
- 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