Timeline for Substructural types, the lambda calculus, and CCCs
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 9, 2017 at 8:22 | comment | added | Mike Shulman | Relevance type systems correspond to relevance monoidal categories. | |
| Jun 7, 2017 at 7:23 | vote | accept | C. Bednarz | ||
| Jun 7, 2017 at 7:18 | answer | added | Peter LeFanu Lumsdaine | timeline score: 0 | |
| Jun 7, 2017 at 7:09 | comment | added | C. Bednarz | @AndrejBauer Just tagged this as a reference-request. Variants of the Curry-Howard correspondence for substructural type systems are exactly what I'm looking for. Thank you | |
| Jun 7, 2017 at 7:06 | history | edited | C. Bednarz |
Tagged as reference-request
|
|
| Jun 7, 2017 at 7:04 | comment | added | Andrej Bauer |
I don't understand what answer we're suposed to give. An entire research overfiew of various variants of the Curry-Howard correspondence for substructural type theory? That's a bit much. Perhaps this should instead be tagged as a reference-request.
|
|
| Jun 7, 2017 at 1:14 | history | edited | C. Bednarz |
edited tags
|
|
| Jun 6, 2017 at 16:16 | comment | added | Damiano Mazza | Affine type systems correspond to what some would call semicartesian closed monoidal categories. The categorical structure associated with relevant type systems probably has no standard name. I suppose it is a symmetric monoidal closed category with suitable natural transformations implementing duplication. For what concerns "ordered" type systems, I don't know exactly, are you talking about subtyping? | |
| Jun 6, 2017 at 2:56 | review | First posts | |||
| Jun 6, 2017 at 3:17 | |||||
| Jun 6, 2017 at 2:54 | history | asked | C. Bednarz | CC BY-SA 3.0 |