Timeline for Proof techniques for showing that dependent type checking is decidable
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 16, 2018 at 14:56 | vote | accept | Joey Eremondi | ||
| Oct 14, 2018 at 3:00 | history | tweeted | twitter.com/StackCSTheory/status/1051306613754253312 | ||
| Oct 11, 2018 at 22:51 | answer | added | cody | timeline score: 9 | |
| Oct 11, 2018 at 6:21 | comment | added | Andrej Bauer | Regarding applying the rules: all term and type rules decrease the goal, except type conversion. Thus we need to control type conversion, which we do by using a bi-directional approach. | |
| Oct 11, 2018 at 6:19 | comment | added | Andrej Bauer | The usual bidirectional type-checking algorithms never attempt to normalize a term (or a type) without first checking that it is well-typed (or well-formed). You need not worry about normalizing untyped terms. | |
| Oct 11, 2018 at 4:59 | history | asked | Joey Eremondi | CC BY-SA 4.0 |