Commits · 312affc1b459d37eef09660b7f449add69882b47 · gradual-typing / sgdt · GitLab

Snippets Groups Projects

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
May 08, 2018
- [coq] start working on the coq impl, but stop · 08f14526
  Max New authored 6 years ago
  
  08f14526
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 03, 2018
- when an F meets a U · 294b2fcb
  Max New authored 6 years ago
  
  294b2fcb
Apr 28, 2018
- [agda] new version of composites, might work? · 53107377
  Max New authored 6 years ago
  
  53107377
Apr 27, 2018
- [agda] change to de bruijn because of better judgmental equality · ee37f2eb
  Max New authored 6 years ago
  
  ee37f2eb
Apr 26, 2018
- start doing the boundary calculuations, a lot of unexpectedly dumb obligations · ff89dff7
  Max New authored 6 years ago
  
  ff89dff7
- most of the multiplicative term lang, val transitivity was hard · 10178f61
  Max New authored 6 years ago
  
  10178f61
Apr 25, 2018
- Add computation transitivity, some sanity checking · 3d3f3e64
  Max New authored 6 years ago
  
  3d3f3e64
- start on agda, coq encodings of gcbpv, use dimension indices! · c2aae633
  Max New authored 6 years ago
  
  c2aae633
Apr 07, 2018
- meeting notes and agdaize cbpv judgmental structure · 3fa7a71f
  Max New authored 6 years ago
  
  3fa7a71f