 Syntax and concepts
 Sugar
This is an extremely quick explanation of Chalf,
a proof editor I have used based on constructive type theory.
As examples, there are scripts for it
here
here
here
here
here
Note that CHalf is obsolete. It is nevertheless
interesting in many ways, and has a very good
implementation by Dan Synek. He wrote it 1995 and justifiably
doesn't want to support it. It is based on ideas and a prototype of Thierry
Coquand. A new typechecker proof assistant called
Agda
has been developed Chalmers.
The semantics is in some ways very intensional, in a manner
reminiscent of MartinLöf type theory from the 70's: it involves the
notion of a closure. (I don't attempt an explanation of the semantics
here.)
CHalf is written in C and emacs lisp and is fast and small. The editing
interface is a standard emacs mode, which is a front end for a
line mode interpreter. It is a simple and elegant tool for carefully
working out definitions and constructive proofs.
Thomas Hallgren in Chalmers has written an experimental GUI called
alfa, which
provides an alternative, sexier environment for proof editing.
Syntax and concepts
In Chalf one has:
 Functions

 functional form:
 ( x : A )> B
 abstraction form:
 \ x > b
 application form:
 b a
 Named products

 product form:
 sig { x1 : A1, .. }
 tuple form:
 struct { x1=a1, .. }
 selection form:
 a.xi
These let you deal with chunkingup blocks
of formal material, and refer to chunk components by name. Note:
the blocks can be empty, as in sig{},struct{}.
 Named sums

 sum form:
 data { $x1 ( y1 : A1, .. , yk : Ak ), .. }
 constructor form:
 $x1 a1 .. ak
 case form:
 case a of { $x1 y1 .. yk > a1, .. }
Facilities for tagging data with named
constructors. Note: there can be zero tags data{}; and a given
tag may have no data data{..,$xi,..}. The behaviour of constructors
with respect to typechecking is extremely subtle. They exhibit a
kind of polymorphism; they are not functions.
 Lets
 let { x1 = a1 : A1, .. } in a
Lets can be recursive: this is combined with `overwriting' in
a syntax which appears to be broken. However one has access to
arbitrary fixedpoint definitions. CHalf has features
that deal with simultaneous definitions, but they appear to
be broken. There is a way to kluge round the bug.
 Sets, Types, Kind, Theories
 Set : Type : Kind, Theory : Kind
 Set, Type, and Kind
are (predicatively) closed under the above constructions.
Theories are collections of definitions of the form theory { x1 =
a1 : A1, .. } , and the definitions within them may be selected
by name as with tuples. Theories are quite difficult to use. One needs
some sugar for introducing their components under new names, such as
is provided by Agda.
Sugar
There is a certain amount of extra sugar that goes with these.
Here is some (I may have forgotten something).
 repeated abstraction form:
 \ x1 .. xk > a is sugar for
\ x1 > .. \ xk > a .
 repeated functional form:
 ( x1 : A1, .. ) > a is sugar for
( x1 : A1 ) > .. > a .
 left hand side parameters:

f ( x1 : A1, .. ) = a : A is sugar for
f = \ x1 .. > a : ( x1 : A1, .. )> A
 use of `useless variables'

In ( x : A )> B, the variable x may not occur in B, so that
one grumbles about having to think of a name. But it is used by the
proof editor as a default, when one sends the checker an Intro
command.
Comments in half are like this { .. }. I am not sure
if they are allowed to be nested.
There is a certain amount of string and sellotape (which works) which
involves lines looking like C preprocessor include lines. This has to
do with loading a selection of files in the right order into the typechecker.
Unfinished bits are represented like this: [].
Sometime I might try to describe what it is the typechecker does.