Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
S
sgdt
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
gradual-typing
sgdt
Commits
cbcbb2555d9510ee58702b93a08974aa283239b5
Select Git revision
Branches
2
main
default
protected
master
2 results
sgdt
code
Author
Search by author
Any Author
authors
darrenwf
darrenwf
ericgio
ericgio
maxsnew
maxsnew
tingtind
tingtind
4 authors
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
Loading