Changelog

Version 1.1.2

• Added Girard's proof of strong normalization of the simply-typed lambda-calculus

Version 1.1.1

• Abella now support mutual induction over specification judgments
• Abella will now issue a warning if a definition might not be stratified
• Better handling of specification contexts when using apply
• The search tactic now takes an optional natural number argument specifying the maximum depth of searching (default 5)
• New examples
  • combinators - correspondence between natural deduction and combinator logic
  • debruijn - translation between higher-order and debruijn lambda terms
  • focus - soundness and completeness for a focused logic

Version 1.1

• Added coinductive definitions and coinduction. These are used through the top-level command CoDefine, which works much like Define, and the tactic coinduction, which is similar to induction but takes no arguments. A brief example of these features is discussed in the Abella reference guide in the section on coinductive restrictions. The following examples are now included in the distribution of Abella.
  • ccs - results on the calculus of communicating systems
  • colist - results on (potentially) infinite lists
  • conat - results on the natural numbers with infinity
  Note: The formal meta-logic underlying Abella with coinduction is still being developed. A paper with the full logic is forthcoming.
• Definitions now support an arbitrary number of nablas in the head.
• The example copy has been updated to show the equivalence of single and double variable definitions of a copy predicate. This is another example of something that is currently impossible to do directly in Twelf.
• Added left and right tactics for selecting the left or right side when the current goal is a disjunction.
• Fixed a bug when case-analysis on a definition with nabla in the head was used multiple times.
• Fixed a bug in the exists tactic where nominal constants were being treated as regular constants.
• Changed the emacs highlighting for Abella. The goal is to highlight the theorems and definitions in a file while downplaying the tactics. Hopefully this makes it easier to skim a file.
• Added more checks to definitions such as preventing the use of undefined predicates and requiring all clauses for a particular predicate to occur together.
• Removed the Axiom command since it can be replaced with a theorem which uses only the skip tactic.

Version 1.0.2

• The search tactic now does a better job of backtracking. In particular, each instantiatable variable is now unbound when the event which caused it to be bound is backtracked over.
• The search tactic now delays conflict pairs which fall outside of the pattern unification fragment. Thus this tactic is now more robust.
• The apply tactic now allows specific instantiations for variables. The general form is

  apply <HYP-NAME> to <HYP-NAMES> with X1 = T1, ..., Xn = Tn.

  where the X1 ... Xn are the variables to be instantiated with T1 ... Tn.
• Randy Pollack has contributed a formalization of the Church-Rosser theorem using Takahashi's proof based on complete developments.

Version 1.0.1

• Slightly extended the ability of the search tactic by adding some corner cases of unification.
• Added definedness and arity checks on the usages of definitions
• The search tactic now uses iterative deepening depth-first search instead of simply depth-first search.
• Fixed some font-locking issues in the emacs files.

Version 1.0

• First public release of Abella