Commits · 01c01516fdc877cfb98a41ebfec1dfa782886836 · 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
- 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
- some comments on the general picture · 2db04def
  Max New authored 6 years ago
  
  2db04def
May 03, 2018
- when an F meets a U · 294b2fcb
  Max New authored 6 years ago
  
  294b2fcb
Apr 29, 2018
- note that the enriched effect calculus types don't seem to work · 394aea9c
  Max New authored 6 years ago
  
  394aea9c
Apr 28, 2018
- more stoupify, multiplicatives and a bit more about models · 0f96c5b1
  Max New authored 6 years ago
  
  0f96c5b1
- [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
- add description of additives · bbc27e35
  Max New authored 6 years ago
  
  bbc27e35
- correct impl of function upcast I think · b6325554
  Max New authored 6 years ago
  
  b6325554
- make upcasts uparrows, dncast down, add model stuff, start function types · 1a8ea286
  Max New authored 6 years ago
  
  1a8ea286
Apr 20, 2018
- add F, U types, prove that they "preserve" upcasts, downcasts resp. · 10deb9d3
  Max New authored 6 years ago
  
  10deb9d3
- meeting notes · 6a2b644b
  Max New authored 6 years ago
  
  6a2b644b
Apr 17, 2018
- judgmental structure and casts for gradual call by push value · e6082718
  Max New authored 6 years ago
  
  e6082718
Apr 07, 2018
- meeting notes and agdaize cbpv judgmental structure · 3fa7a71f
  Max New authored 6 years ago
  
  3fa7a71f
Apr 06, 2018
- universal property for products · 757bfea7
  Max New authored 6 years ago
  
  757bfea7
- fix ret · 27b7ba92
  Max New authored 6 years ago
  
  27b7ba92
Apr 04, 2018
- threeorders don't work · 13891ff8
  Max New authored 6 years ago
  
  13891ff8
Apr 03, 2018
- start writing up judgmental structure · dc32ef2f
  Max New authored 6 years ago
  
  dc32ef2f
- right definition of non-multicategory version of the type theory · d8264b00
  Max New authored 6 years ago
  
  d8264b00
Apr 02, 2018
- notes on "Exploring the Design Space" and how it relates · 31b540ec
  Max New authored 6 years ago
  
  31b540ec
- define free freyd category, conjecture about preorder version · fea7db8c
  Max New authored 6 years ago
  
  fea7db8c
- compile command · 8c22f2f6
  Max New authored 6 years ago
  
  8c22f2f6
Mar 30, 2018
- start definition of freyd categories as generalized multicategories · 62e9af5e
  Max New authored 6 years ago
  
  62e9af5e