Wen Kokke
|
f04dbd2c65
|
Updated Lambda to specify determinism implies the diamond property and confluence, but the diamond property does not imply confluence by itself.e
|
2020-07-13 15:03:00 +01:00 |
|
Wen Kokke
|
8d59de6394
|
Added rewrite of Inference by Prabhakar
|
2020-05-22 15:50:50 +01:00 |
|
wadler
|
f2cb91fc30
|
added Levy suggestion to extra
|
2020-04-30 08:36:48 -03:00 |
|
Georgi Lyubenov
|
ef7f95b1db
|
Make sum type right-associative
|
2019-12-02 09:49:49 +02:00 |
|
wadler
|
2a68a579fb
|
extra files
|
2019-10-14 12:18:28 +01:00 |
|
Wen Kokke
|
f20abd92eb
|
Restructured directory.
|
2019-08-15 17:26:21 +01:00 |
|
Philip Wadler
|
de2d4112e3
|
completing merge
|
2019-07-22 17:56:39 +01:00 |
|
wadler
|
90ce509af6
|
small changes
|
2019-07-13 20:46:33 -03:00 |
|
Marko Dimjašević
|
3e07764efe
|
Quantitative: fixes a spelling error
|
2019-06-20 14:00:41 +02:00 |
|
Reza Gharibi
|
5851f261eb
|
Replaced 'De Bruijn' with 'de Bruijn'
|
2019-06-15 18:33:21 +02:00 |
|
Jeremy Siek
|
ed1d572450
|
alternative to BCD subtyping
|
2019-06-13 13:44:19 -04:00 |
|
Jeremy Siek
|
18cec9a0da
|
moving denotational back to plfa, updates to Confluence
|
2019-05-25 16:11:01 -04:00 |
|
Jeremy Siek
|
fcfcd2a70c
|
fixed Soundness and updates some text
|
2019-05-25 13:01:04 -04:00 |
|
wadler
|
80398ee5e2
|
temporary move denotational to extra
|
2019-05-25 10:47:23 -03:00 |
|
Jeremy Siek
|
afbd8e8735
|
really moving confluence
|
2019-05-13 16:31:52 -04:00 |
|
Jeremy Siek
|
d65623e67c
|
moving confluence to src/plfa
|
2019-05-13 16:31:30 -04:00 |
|
Jeremy Siek
|
ff7f4f8163
|
getting ready to move Substitution, LambdaReduction, and CallByName to plfa
|
2019-05-13 16:24:19 -04:00 |
|
Jeremy Siek
|
b7dd252cea
|
cleaning up imports
|
2019-05-12 11:19:05 -04:00 |
|
Jeremy Siek
|
bed038d076
|
lots of cleanup and some added text
|
2019-05-12 07:02:08 -04:00 |
|
Jeremy Siek
|
a9dfedc514
|
text and cleanup for Substitution
|
2019-05-11 17:50:24 -04:00 |
|
Jeremy Siek
|
9b40bb0735
|
a little more text
|
2019-05-09 20:52:14 +02:00 |
|
Jeremy Siek
|
89b647b09d
|
minor edits
|
2019-05-09 08:40:32 +02:00 |
|
Jeremy Siek
|
5add203818
|
worked around eta issue
|
2019-05-09 08:36:06 +02:00 |
|
Jeremy Siek
|
df6ca9bec4
|
more house cleaning
|
2019-05-09 08:22:11 +02:00 |
|
wadler
|
b2c9e3099d
|
updated Confluence
|
2019-05-08 16:49:12 -03:00 |
|
wadler
|
84aa286783
|
updated Confluence
|
2019-05-08 16:39:06 -03:00 |
|
Jeremy Siek
|
ddc143672a
|
added some notes
|
2019-05-08 21:09:22 +02:00 |
|
Jeremy Siek
|
388b64a2de
|
minor edits
|
2019-05-08 19:54:27 +02:00 |
|
Jeremy Siek
|
6fc3e4a920
|
finished main text for confluence
|
2019-05-08 18:01:32 +02:00 |
|
Jeremy Siek
|
f8ed0b378f
|
adding text to proof of confluence
|
2019-05-08 17:43:39 +02:00 |
|
Jeremy Siek
|
62b9bc0a75
|
split out reduction rules
|
2019-05-08 15:22:29 +02:00 |
|
Jeremy Siek
|
6d9999bb73
|
finished confluence!
|
2019-05-08 14:05:30 +02:00 |
|
Jeremy Siek
|
49aba03101
|
finished subst-par lemma and the substitution lemmas it depends on
|
2019-05-08 10:53:14 +02:00 |
|
Jeremy Siek
|
a03eb20083
|
progress
|
2019-05-07 20:39:13 +02:00 |
|
Jeremy Siek
|
b4c8986009
|
some progress on confluence
|
2019-05-07 12:01:20 +02:00 |
|
Jeremy Siek
|
2e999b167e
|
minor tweak
|
2019-05-06 15:19:40 +02:00 |
|
Jeremy Siek
|
5070619dd9
|
removed some dead code
|
2019-05-06 15:15:54 +02:00 |
|
Jeremy Siek
|
4658c1e275
|
minor tweak
|
2019-05-06 15:01:34 +02:00 |
|
Jeremy Siek
|
27983098b0
|
remove obsolete file
|
2019-05-06 14:59:59 +02:00 |
|
Jeremy Siek
|
7b088da512
|
finished call-by-name soundness
|
2019-05-06 14:59:04 +02:00 |
|
Jeremy Siek
|
08a7121235
|
new file
|
2019-05-03 14:01:46 +02:00 |
|
Wen Kokke
|
62d742a549
|
Brought QTT up to speed more or less with a taste of linear logic
|
2019-03-16 11:00:08 +01:00 |
|
Wen Kokke
|
8e66074a2b
|
Finished adding units, products, and sums to QTT
|
2019-03-12 11:31:36 +01:00 |
|
Wen Kokke
|
647f71bbd5
|
making progress towards qtt/more
|
2019-03-10 20:20:20 +01:00 |
|
Wen Kokke
|
888b67e6f2
|
Moved QTT to extra
|
2019-03-10 20:20:20 +01:00 |
|
Marko Dimjašević
|
aa1a49d336
|
Capitalises 'cartesian'
|
2019-01-25 23:34:26 +00:00 |
|
Marko Dimjašević
|
6ec9eea5c8
|
Decidables: adds a word fix to a version under extra
|
2019-01-25 23:31:55 +00:00 |
|
Marko Dimjašević
|
2a33fefab0
|
Lists: fixes spellings of several words
|
2019-01-25 23:31:32 +00:00 |
|
Marko Dimjašević
|
e3623f18cb
|
Lambda: fixes spellings of a few words
|
2019-01-25 23:31:10 +00:00 |
|
Marko Dimjašević
|
c5f862ecfa
|
Properties: fixes spellings of a few words
|
2019-01-25 23:30:45 +00:00 |
|