Timeline for Is there an easy decision algorithm for the inhabitation problem for simple types?
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 24, 2015 at 23:58 | answer | added | lukasz | timeline score: 2 | |
| Aug 21, 2013 at 23:20 | history | edited | Alfie | CC BY-SA 3.0 |
added 10 characters in body
|
| Aug 21, 2013 at 23:12 | comment | added | Alfie | @AndrejBauer Also you usually assume the existence of a countably infinite set of atomic types, but I don't think it's too important for this. | |
| Aug 21, 2013 at 23:08 | comment | added | Alfie | Maybe it's not, but why do you need to use the full power of the Curry-Howard isomorphism, when you have this nice syntactical proof? | |
| Aug 21, 2013 at 23:06 | comment | added | Alfie | @AndrejBauer I'm sorry I mean the basic system of simply typed $\lambda$-terms with just typing rules of arrow introduction, arrow elimination and variable. Do I need to be more specific? | |
| Aug 21, 2013 at 22:54 | comment | added | Andrej Bauer | How is what you are talking about different from a decision procedure for provability of formulas in intuitionistic propositional calculus? | |
| Aug 21, 2013 at 22:53 | comment | added | Andrej Bauer | Can you be a bit more specific about your type theory? Not everyone know what $TA_\lambda$ is supposed to be. Are there basic types? Are there sums and the empty type? | |
| Aug 21, 2013 at 22:36 | history | edited | Alfie | CC BY-SA 3.0 |
deleted 58 characters in body
|
| Aug 21, 2013 at 19:58 | review | First posts | |||
| Aug 21, 2013 at 20:04 | |||||
| Aug 21, 2013 at 19:41 | history | asked | Alfie | CC BY-SA 3.0 |