CL   Programming Language and Proof Assistant

What is CL?

CL (Clausal Language) is a declarative programming language with the look and feel of a modern functional programming language. CL identifies the domain of symbolic expressions of LISP with the domain of natural numbers. Functions and predicates of CL are recursive functions and predicates over natural numbers. The coding comfort of LISP is achieved with the help of a pairing function. For more details see the short paper Computer Programming as Mathematics, or Metamathematics of Computer Programming (extended introduction).

CL has its own intelligent proof assistant

CL comes with its own proof system (intelligent proof assistant) in which the user can state and prove properties of his functions and predicates. The formal system is Peano arithmetic. (PA). See the text Specification and Verification of Programs. by J. Komara for an extensive collection of definitions and proofs in PA. The text is used in an undegraduate course with the same title and contains specifications, definitions in CL, and proofs in PA of about 400 hundred functions and predicates. The students are expected to define and verify the CL programs in the system CL.

How to run CL?

A web version of CL runs on Intel-based computers running Linux or Windows. CL executes as a server accessed through a web browser supporting MathML, for instance Mozilla. CL programs extensively use the mathematical symbols of MathML and your browser should have the mathematical fonts installed. Instructions for installing the mathematical fonts into Mozilla are here.

• You can experiment with the system CL without downloading it by runnning the CL server remotely on our computer. The server runs the full CL system but for security reasons you are not allowed to write to any files and so you will not be able to save your work. The online version of CL is accessed from here.

• In order to make the full use of CL you should download the system to your computer and run the CL server locally. Instructions for downloading the system CL are here.

What do we use CL for?

If you wish to see the courses currently taught with CL in Bratislava go here.

CL at DIKU in Copenhagen

If you wish to see how CL has been used in a course taught in the Fall term 2002 at the University of Copenhagen, go to the main page of the course: Metamathematics of computer programming.

The work on the next version of CL

We are currently in the last phase of research into the design of a successor to CL, with a working name NCL (New CL). The work on its implementation should start in the Fall of 2003. There will be three major innovations in CL, each of which is described in a separate research paper.

Modularity

In order to implement the modularity which calls for parameterization/quantification by functions and predicates we have to move from the first-order theory of arithmetic (PA) to a subsystem of the second-order arithmetic. The most suitable such system is called ACA₀ and it is used in the so-called Reverse mathematics. ACA₀ is one of the weakest extensions of PA into second-order because it is conservative over PA. The paper Grundlagenstreit in the Theory of Programming by P. J. Voda describes the overall filosophy of the extension together with a critique of alternative approaches to the theory of programming. The paper Predicative Justification and Development of a Second Order Theory of Finite Sets by P. J. Voda describes the intended formal theory of NCL called FSI (Finite Sets with Induction). The theory is equivalent to ACA₀.

Syntactic Extensibility

Programs of CL are totally expressed within the language of PA (or FSI). The paper What Can we Gain by Integrating a Language Processor with a Theorem Prover? by P. J. Voda describes a method of extending the syntax of CL, which will still remain within the language of PA (FSI), but it will permit definitions of user-defined discrimination (case analysis) constructs. User-defined discriminations afford a powerful generalization of (non-extensible) pattern matching as it is known from the declarative programming languages and also used in the current version of CL.

The cited paper contains also the full description of semantics of CL. It specifically describes the reduction of clausal definitions to extensions of PA by definitions. It also formally describes the execution (reduction) of computable CL definitions.

Specification of representation and translation to machine level

CL (and NCL) are both typeless languages. This is because also PA is typeless. The paper From Declarative to Imperative Proof-Carrying Programs by Jan Kluka and P. J. Voda describes a sublanguage of CL, called Peano Pascal (PP) which is so close to the machine level that it can be directly transformed to the machine language. PP affords extensibility in definitions of PP-types by allowing description of methods of representing subsets of natural numbers in the computer store. It will be possible to describe via PP-typing of NCL programs their translation into PP and from there to machine code.

The interesting thing on this approach is that the translator can automatically formulate and prove correctness properties of transformed PP programs. The CL-to-PP translation permits also the specification of reuse of the store which leads to efficient programs implementing, for instance, lists by arrays.