Masami Hagiya
hagiya@is.s.u-tokyo.ac.jp
Higher-order typed lambda-calculi, including Calculus of Constructions, are also called general logic or logical framework, because they can be used as a general framework to implement various kinds of logical system such as first-order predicate calculus. This means that representing a proposition of a logical system as a type and a proof as a lambda-term by the Curry-Howard correspondence, one can implement the logical system on a higher-order typed lambda-calculus. Consequently, by typechecking a lambda-term, one can check a proof that is represented by the lambda-term. In recent years, many proof-checkers based on higher-order typed lambda-calculi have been developed, and higher-order typed lambda-calculi have become a standard framework for writing formal proofs.
Extended Calculus of Constructions, proposed by Zhaohui Luo, is an extension of Calculus of Constructions by Sigma-types and a type hierarchy. Boomborg-PC can also typecheck lambda-terms in a subsystem of Extended Calculus of Constructions.
On the other hand, GNU Emacs is a general-purpose text editor developed by Richard Stallman, and has become a standard text editor on workstations. Nemacs, the Japanese version of GNU Emacs, developed by Ken'ichi Handa et al., and its descendant Mule, the multilingual enhancement to GNU Emacs, are also widely used as a Japanese text editor.
Boomborg-PC is a typechecker in which one can typecheck lambda-terms of Calculus of Constructions on a buffer of Mule or Nemacs. The characteristic features of Boomborg-PC as a proof-checker can be summarized as follows.
Feedbacks from the proof-checker are inserted into the editor buffer and can be used as parts of the proof being constructed.
The proof-checker also supports interactive proof construction by having commands to insert proof templates into the buffer.
The proof-checker does not have any state other than the proof text on the buffer. Therefore, a proof can be immediately checked after modification of any part of the proof.
Since the proof-checker only does minimal analysis of the structure of a proof, incompletely constructed proofs can also be checked.