Barista Homepage
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