lambdacalculator
commented
7 years ago One useful model to keep in mind here might be Twelf. There, you can put certain stylized comments in your source that initiate certain checks on the specification as it is being read, in particular %mode, %terminates, %reduces, and %total. That way, the user has complete control over the extra checks that are run, and in a localized way. In Abella, each one of these checks corresponds to a particular theorem, so another intriguing possibility here would be to add such checks as Abella commands that, if they succeed, add the corresponding new theorems (whose proofs always follow a standard template) to the session and print them out for future reference.
As I give thought to some forms of static analysis for λProlog code, I realize it could be interesting to run some such checks when we import a specification in Abella (beyond the usual syntactic checks that are already in place). These need not result in hard errors, but warnings about unused variables or constructors, possibly nonterminating behavior, etc., would be useful to have.
I am already working on this, because Abella gives me a convenient framework to experiment. If there is no interest whatsoever in seeing this in master, I can dismantle this in a branch for my purposes, but otherwise I would be happy to argue for it and submit a set of checks of interest to the mainline.