Changelog

Version 1.3.1

• Fixed a variable capture bug when using apply.

Version 1.3

This version of Abella introduces simple-typing. This might be best illustrated by an example such as examples/type-uniq. Further documentation is available in the reference guide section on typing.

• The syntax of definitions has been changed so that all clauses are listed in a single command. See examples/type-uniq. for an example.
• Added the backchain tactic which is in some sense dual to the apply tactic. The backchain tactic applies a lemma (or hypothesis) to the current goal and produces new subgoals for each of the hypotheses to the lemma.
• Added the permute tactic which permutes the nominal constants in a hypothesis or goal.
• Improved the handling of non-Lλ unification and constraints. After case analysis, lingering constraints are added as equality hypotheses.
• Added Quit command.
• Added a development of some meta-theory of the π-calculus contributed by Dale Miller.
• Added a development which showcases some of the higher-order logic programming features which are available in Abella's specification logic.

Version 1.2

This version of Abella is aimed at supporting larger developments. Most notably, it introduces a way to compile and import developments. This requires a change to way specifications are associated with developments which is not backwards compatible. All of the examples have been updated to this new style.

• Specifications are now explicitly loaded into a development via the Specification command as described here.
• Developments may now be compiled and imported into other developments as described here.
• The Query command allows the animation of definitions as described here.
• Command line options have been reorganized. Run abella --help to find out more.
• Some run-time options may be configured via the Set command as described here.
• Subgoals now use hierarchical numbering.
• Large hypotheses may now be abbreviated using the abbrev and unabbrev commands as described here.
• Multi-line comments are now supported via /* ... */. These comments may be nested.
• The annotations for co-induction now use # and + to avoid confusion with the annotations for induction (@ and *).

Version 1.1.3

• The split tactic now operates on n-ary conjunctions
• Tactic names no longer conflict with terms during parsing
• Added the monotone tactic which explicitly realizes the monotonicity property of specification logic contexts
• Fixed a couple unification bugs
• New examples
  • path - equivalence of lambda terms based on the paths through terms
  • cut - this cut admissibility example has been updated to include all operators of the sequent calculus
  • pi - specification of late pi-calculus and strong bisimulation

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