james
/
darius
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
23 Commits
1 Branch
0 Tags
193 KiB
master
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Commit Graph

23 Commits (master)
 

Author SHA1 Message Date
James T. Martin bb53c1b162
WIP C bootstrap VM of a classical linear language. 11 months ago
James T. Martin 88e9dabddf
A few small random old things. 1 year ago
James T. Martin 65ac3994b8
It works! It works! (LEM-based assembly coroutines.) 1 year ago
James T. Martin edfa1c3c00
WIP assembly implementation of classical linear semantics. 1 year ago
James T. Martin 757e4a5f6d
Basic-ally pain and suffering. 1 year ago
James T. Martin 2b585cd1ae
Not sure. Some basic-related stuff. 1 year ago
James T. Martin 5a8eca0481
WIP basic logic cuts 1 year ago
James T. Martin 9efab5e286
Does substitution finally compute definitionally? I believe it will! 
I've learned a lot about maximizing laziness and its
relation to getting shit to compute on open terms over
these last few days. I believe this lesson will remain relevant
for many years to come.

Also, deleted zipper because I'm pretty sure it can't be made
lazy even in principle, and therefore it is useless.
 1 year ago
James T. Martin 36333b9537
I forgot lol 1 year ago
James T. Martin eb28c76b1b
Finally got my stupid freaking constructors to compute! 1 year ago
James T. Martin 5df3d65042
Why won't my shit compute!? (p.s. equality is the root of all evil.) 1 year ago
James T. Martin 4e3698ed84
Agonizingly tediously moving stuff to use new subst. 1 year ago
James T. Martin 9bb12148b5
Substitution, attempt 4-ish? Prev was too complicated for proofs. 
(This one is quite nice! And I actually understand how it works.)
 1 year ago
James T. Martin b0a3938db8
Proved unique typing, unique type derivations, & subject reduction. 1 year ago
James T. Martin bb5116e951
Typed reduction derivations (again). 1 year ago
James T. Martin 88fe4fdc8f
Typed substitution: finally correct? 1 year ago
James T. Martin 174c45ac01
Frustrating broken crap. 1 year ago
James T. Martin 6616128f73
Added typing judgements and untyped reduction. 1 year ago
James T. Martin 8ccb5f0c26
New substs which will hopefully work maybe. 
It's much more general and less ad-hoc.
On the other hand, I have no idea how it works (or if it works).
I derived it pretty much by just writing out the type and putting
in whatever I hoped would make the typechecker happy.

I came up with that particular type signature by working on
the new linear derivations, which require much more sophisticated
types of substitution than I originally accounted for. I believe
substs will be sufficiently general (if it works!!).
 1 year ago
James T. Martin 45ca5caec9
Linear substitution for linear terms which *hopefully* works. 1 year ago
James T. Martin 360cfec241
Partial work towards normalization (not much). 1 year ago
James T. Martin 47be20183f
Improving the formulation of derivations. 1 year ago
James T. Martin 1b85cbbd0d
Defining terms and conversions for dependent type theory. 1 year ago