summaryrefslogtreecommitdiffstats
path: root/content/zettel/2e1c1a.md
diff options
context:
space:
mode:
Diffstat (limited to 'content/zettel/2e1c1a.md')
-rw-r--r--content/zettel/2e1c1a.md18
1 files changed, 18 insertions, 0 deletions
diff --git a/content/zettel/2e1c1a.md b/content/zettel/2e1c1a.md
new file mode 100644
index 0000000..3ea908b
--- /dev/null
+++ b/content/zettel/2e1c1a.md
@@ -0,0 +1,18 @@
++++
+title = "Proof carrying scheduling"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["2e1c1"]
+forwardlinks = []
+zettelid = "2e1c1a"
++++
+
+Another option to prove this theorem would be to have proof carrying
+scheduling, which gives information to the checker about which
+transformations took place, so that these can be reversed, if possible,
+to get a syntactically equal representation.
+
+However, the main problem with this, is that it is quite difficult to
+even identify the different translations that were done to the
+predicates, and it may not really help the proof.