Timeline for Typed Lambda Calculus models and denotations
Current License: CC BY-SA 3.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 30, 2016 at 14:34 | history | tweeted | twitter.com/StackCSTheory/status/770630894788960256 | ||
| Aug 30, 2016 at 12:16 | comment | added | Andrej Bauer | Maybe Paul Taylor's Appendix A of paultaylor.eu/stable/prot.pdf, that's a classic. If you want to dive into category theory you could try the recent paper by Ghani, Nordvall and Simpson (link.springer.com/chapter/10.1007%2F978-3-662-49630-5_1 or pure.strath.ac.uk/portal/en/publications/… for a pdf) | |
| Aug 29, 2016 at 20:07 | comment | added | chi | @AndrejBauer Would you recommend starting from any particular approach, even if abstract, for System F? | |
| Aug 29, 2016 at 18:58 | comment | added | Andrej Bauer | For System F things are a bit more complicated. There's usually more category theory involved. | |
| Aug 29, 2016 at 18:35 | comment | added | Martin Berger | @chi We have a draft here. It's not a very well-developed approach currently. | |
| Aug 29, 2016 at 18:30 | comment | added | chi | @AndrejBauer Thanks. The first random paper I just browsed used a shallow approach to polymorphism: intersect all the PERs for every $\tau$ ranging over monotypes. I'll look further to find something deeper, so to encompass e.g. System F. | |
| Aug 29, 2016 at 18:26 | comment | added | chi | @MartinBerger You mean to interpret a lambda term as a (ordered) set of formulae? I'm trying to figure out how that would work... | |
| Aug 29, 2016 at 17:31 | comment | added | Martin Berger | @chi How about logical formulae ordered by implication? | |
| Aug 29, 2016 at 16:44 | comment | added | chi | @MartinBerger Good point. I guess I have a bias towards domain-theoretic semantics (à la Winskel's book) since I want to handle non-termination. I'm also willing to explore set-theoretical models for some terminating fragment, especially if they can be extended to cover non-termination as well. I'm not much familiar on those at the moment, though. | |
| Aug 29, 2016 at 15:46 | comment | added | Martin Berger | @chi, what do you count as denotational semantics? | |
| Aug 29, 2016 at 13:01 | comment | added | Andrej Bauer | PER models seem like a natural next thing to study. | |
| Aug 29, 2016 at 12:43 | review | First posts | |||
| Aug 29, 2016 at 15:47 | |||||
| Aug 29, 2016 at 12:41 | history | asked | chi | CC BY-SA 3.0 |