summaryrefslogtreecommitdiffstats
path: root/content/zettel/3a8g5h5.md
diff options
context:
space:
mode:
Diffstat (limited to 'content/zettel/3a8g5h5.md')
-rw-r--r--content/zettel/3a8g5h5.md18
1 files changed, 18 insertions, 0 deletions
diff --git a/content/zettel/3a8g5h5.md b/content/zettel/3a8g5h5.md
new file mode 100644
index 0000000..63b4610
--- /dev/null
+++ b/content/zettel/3a8g5h5.md
@@ -0,0 +1,18 @@
++++
+title = "Syntactic checks"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g5h4", "3a8g5g1"]
+forwardlinks = ["3a8g5h6"]
+zettelid = "3a8g5h5"
++++
+
+Prove the Tarjan algorithm and get a syntactical proof that they will be
+independent and correct. This will then allow one to make syntactic
+statements about the predicates, which can be much more useful than the
+abstract statements that are currently made.
+
+In addition to that, one problem is that currently the proof does not
+have a notion of post-dominance, which seems to be necessary to reason
+about these predicates in a syntactic manner.