Barista is an Italian word for the espresso server (the coffee guy
behind the counter) and for us stands for the generic proof server
program. It is a TCP/IP socket program written in Java. A
barista server 1) keeps listening to the designated port, 2) starts
a proof checker process for each socket, 3) receives proof scores
through the socket, 4) passes them to the proof checker, and 5)
returns the result to the client. Since the communication between
the server and the proof checker is done by standard input and
output, any type of proof checker programs can be used. The
client program only needs to send and receive messages through
sockets, i.e, there is no preprocessor or modifier, however,
simple filters may be attached in the server program.
The source code of the barista proof server is available here. Although it is tailored for
OBJ3, it can be easily modified for any other systems. Please
refer to the comments in the source code.
Also a simple client program (a Java applet) used in the handmade demo examples can be obtained here.
20 February 1998