+++
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.