Location: Dept. of Appl. Inf. (AI and DP) | Faculty of Math., Physics, and Inf. | Comenius Univ. Bratislava | Slovakia

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.

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.


* – updated within last 7 days Last modified: 2006-12-01T13:58+0100