yellowsquid/church-eval.git/src, branch semantics-with-proof [no description] http://git.yellowsquid.uk/yellowsquid/church-eval.git/atom?h=semantics-with-proof 2023-06-22T12:52:03Z WIP: define semantics in Idris. 2023-06-22T12:52:03Z Chloe Brown chloe.brown.00@outlook.com 2023-06-22T12:52:03Z urn:sha1:41d1c4a059466833325320e1d494d99af9d36cb2 Add sums, vectors and arithmetic encodings. 2023-06-21T15:05:44Z Chloe Brown chloe.brown.00@outlook.com 2023-06-21T15:05:44Z urn:sha1:0ddaf1b2c9ca66cf0ae03d2f6ad792c7885dfc32 Also define pretty printing of terms. Define semantics and encode types up to pairs. 2023-06-16T17:01:33Z Chloe Brown chloe.brown.00@outlook.com 2023-06-16T17:01:33Z urn:sha1:af7c222cc3e487cd3ca8b5dd8749b7e258da7c7c Reset using only co-de Bruijn syntax. 2023-06-16T14:06:59Z Chloe Brown chloe.brown.00@outlook.com 2023-06-16T14:06:59Z urn:sha1:5adc1ae9357e42937a601aab57d16b2190e10536 Use co-deBruijn syntax in logical relation proof. 2023-06-09T15:00:39Z Chloe Brown chloe.brown.00@outlook.com 2023-06-09T15:00:39Z urn:sha1:f910e142ce7c10f8244ecfa40e41756fb8c8a53f Many proofs are still missing. Because they are erased, the program still runs fine without them. Use CoDebruijn syntax at top level. 2023-06-08T16:17:04Z Chloe Brown chloe.brown.00@outlook.com 2023-06-08T16:17:04Z urn:sha1:d5794f15b40ef4c683d713ffad027e94f2caf17e Fully expand thinnings. 2023-06-08T13:23:29Z Chloe Brown chloe.brown.00@outlook.com 2023-06-08T13:23:29Z urn:sha1:c64650ee0f41a1ebe45cf92c9b999f39825e9f5e This makes adding CoDebruijn syntax simpler. If carrying the lengths of contexts around is too inefficient, I can always switch back to truncated thinnings. Add a pretty printer. 2023-06-06T14:13:22Z Chloe Brown chloe.brown.00@outlook.com 2023-06-06T14:13:22Z urn:sha1:6590816a835110b8181472a5116dd4ecf67c957c Write an encoding for data types. 2023-06-06T11:25:26Z Chloe Brown chloe.brown.00@outlook.com 2023-06-06T11:25:26Z urn:sha1:bf07a9fe3ee4ff06fe186e33221f7f91871b9217 Give a logical relation template. 2023-06-01T16:07:41Z Chloe Brown chloe.brown.00@outlook.com 2023-06-01T16:07:41Z urn:sha1:d5f8497dbb6de72d9664f48d6acbc9772de77be3