yellowsquid/cfe-proof.git/src/Cfe/Judgement, branch cleanup [no description] http://git.yellowsquid.uk/yellowsquid/cfe-proof.git/atom?h=cleanup 2021-04-24T12:55:59Z Reprove properties of the typing judgement. 2021-04-24T12:55:59Z Chloe Brown chloe.brown.00@outlook.com 2021-04-24T12:55:59Z urn:sha1:c58866bea6ee251868d98a3da11f64030bb00aa7 Introduce non-terminating proof of derivation existence. 2021-03-27T20:32:03Z Chloe Brown chloe.brown.00@outlook.com 2021-03-27T20:32:03Z urn:sha1:adad5280af0d81a2f171df619e9c7169dcb43a02 Prove soundness of judgement. 2021-03-27T14:50:17Z Chloe Brown chloe.brown.00@outlook.com 2021-03-27T14:50:17Z urn:sha1:b254d61d3a4084e0f2dc47cded5b4482cc31ae23 Begin soundness proof. 2021-03-27T13:34:32Z Chloe Brown chloe.brown.00@outlook.com 2021-03-24T09:30:13Z urn:sha1:a95622ca33a31a8c6d3cb31c7ca3b390e7aa5624 Prove substitution into guarded variable. 2021-03-23T14:14:17Z Chloe Brown chloe.brown.00@outlook.com 2021-03-23T14:14:17Z urn:sha1:da0c9709fc93676587c1505de688d7d1f7a33489 Replace transfer with shift. 2021-03-23T12:19:30Z Chloe Brown chloe.brown.00@outlook.com 2021-03-23T12:19:30Z urn:sha1:a92f724a46a78af74121c44bbb06c4ec51f9555e Prove substitution in the unguarded context. Prove transfer. 2021-03-22T16:43:49Z Chloe Brown chloe.brown.00@outlook.com 2021-03-22T16:43:49Z urn:sha1:9e89f36e3fc6210b270d673c30691530015278fb Prove judgement weakening. 2021-03-21T13:14:22Z Chloe Brown chloe.brown.00@outlook.com 2021-03-21T13:14:22Z urn:sha1:9c72c8ed0c3e10b5dafb41e438285b08f244ba68 Separate Context into a different module. 2021-03-20T18:36:24Z Chloe Brown chloe.brown.00@outlook.com 2021-03-20T18:36:24Z urn:sha1:4e0ceac75e6d9940f0e11f93a3815448df258c70 Change judgement to use variable contexts. 2021-03-20T18:18:31Z Chloe Brown chloe.brown.00@outlook.com 2021-03-20T18:18:31Z urn:sha1:16afd9dff6798509a1d654b0f06e409353e01180 Add some useful context transformations.